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.
Editor(s) Uwe Brahm | Created 03/25/1996 06:14:18 PM | |
Revisions 2. 1. 0. | Editor(s) Anja Becker Uwe Brahm Uwe Brahm/MPII/DE | Edit Dates 08.07.2011 13:27:53 03/23/98 07:28:51 PM 03/25/96 06:16:15 PM |