Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt





Contextual Rewriting in SPASS


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

Wischnewski, P. (2007). Contextual Rewriting in SPASS. Master Thesis, Universität des Saarlandes, Saarbrücken.

First-order theorem proving with equality is undecidable, in general. However, it is semi-decidable in the sense that it is refutationally complete. The basis for a (semi)-decision procedure for first-order clauses with equality is a calculus composed of inference and reduction rules. The inference rules of the calculus generate new clauses whereas the reduction rules delete clauses or transform them into simpler ones. If, in particular, strong reduction rules are available, decidability of certain subclasses of first-order logic can be shown. Hence, sophisticated reductions are essential for progress in automated theorem proving. In this thesis we consider the superposition calculus and in particular the sophisticated reduction rule Contextual Rewriting. However, it is in general undecidable whether contextual rewriting can be applied. Therefore, to make the rule applicable in practice, it has to be further refined. In this work we develop an instance of contextual rewriting which effectively performs contextual rewriting and we implement this in the theorem prover Spass.