Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Contextual Rewriting in SPASS

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

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-1D89-6 Versions-Permalink: https://hdl.handle.net/21.11116/0000-0003-012D-A
Genre: Hochschulschrift

Dateien

einblenden: Dateien
ausblenden: Dateien
:
master.pdf (Verlagsversion), 5KB
 
Datei-Permalink:
-
Name:
master.pdf
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Privat
MIME-Typ / Prüfsumme:
application/pdf
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Wischnewski, Patrick1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2008-02-282007-09-292007
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: Saarbrücken : Universität des Saarlandes
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 356454
Anderer: Local-ID: C12573CC004A8E26-4510F08E286235C1C12573D4004FF8F5-Wischnewski2007
 Art des Abschluß: Master

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle

einblenden: