English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

Transformations of First-Order Formulae for Automated Reasoning

MPS-Authors
/persons/resource/persons45301

Rock,  Georg
Programming Logics, MPI for Informatics, Max Planck Society;

External Ressource
No external resources are shared
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Rock, G. (1995). Transformations of First-Order Formulae for Automated Reasoning. Master Thesis, Universität des Saarlandes, Saarbrücken.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-AC2F-E
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.