de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Hochschulschrift

Transformations of First-Order Formulae for Automated Reasoning

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45301

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


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