Instance Generation Methods for Automated Reasoning

Jacobs, Swen

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Thesis

Instance Generation Methods for Automated Reasoning

MPS-Authors

/persons/resource/persons44687

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

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

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: https://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.