Item

Abstract

Theorem prover for first-order logic usually operate on a set of clauses.
Since it is more natural and adequate to code problems in full first-order
logic, the problem of translating a formula into clause normal form
is an important one in this field. From experience we know that a theorem
prover can find a
proof more easily with a compact clause normal form than with a huge set of
clauses.
In this thesis we present powerful methods to obtain compact clause normal
forms.