Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Hochschulschrift

Labelled Splitting

MPG-Autoren
/persons/resource/persons44415

Fietzke,  Arnaud
Automation of Logic, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-1D84-0
Zusammenfassung
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.