Rock, Georg

Transformations of First-Order Formulae for Automated Reasoning

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.