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

Item

ITEM ACTIONSEXPORT

Released

Thesis

Labelled Splitting

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

Fietzke,  Arnaud
Automation of Logic, MPI for Informatics, Max Planck Society;
International Max Planck Research School, 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

Fietzke, A. (2007). Labelled Splitting. Master Thesis, Universität des Saarlandes, Saarbrücken.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-1D84-0
Abstract
Saturation-based theorem provers are typically based on a calculus consisting of inference and reduction rules that operate on sets of clauses. While inference rules produce new clauses, reduction rules allow the removal or simplification of redundant clauses and are an essential ingredient for efficient implementations. The power of reduction rules can be further amplified by the use of the splitting rule, which is based on explicit case analysis on variable- disjoint components of a clause. In this thesis, I give a formalization of splitting and backtracking for first-order logic using a labelling scheme that annotates clauses and clause sets with additional information, and I present soundness and completeness results for the corresponding calculus. The backtracking process as formalized here generalizes optimizations that are currently being used, and I present the results of integrating the improved backtracking into SPASS.