de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

Instance Generation Methods for Automated Reasoning

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44687

Jacobs,  Swen
Automation of Logic, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Jacobs, S. (2004). Instance Generation Methods for Automated Reasoning. Diploma Thesis, Universität des Saarlandes, Saarbrücken, Saarland.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-2548-4
Abstract
There are several different methods which try to decide unsatisfiability of a set of clauses by generating an unsatisfiable set of instances of the input clauses. We consider the \emph{Disconnection Tableau Calculus}, \emph{Primal Partial Instantiation} and \emph{Resolution-Based Instance-Generation}, all of which can be seen as refinements of the clause linking approach. We present these three methods accurately and in a consistent manner. Similarities and equivalences of the methods will be pointed out and we will show if proofs of one calculus can be simulated by a different method, generating only instances from the given proof.