Vergleich und Analyse von Ordnungseinschränkungen für freie Variablen Tableau

In dieser Arbeit untersuchen wir einige Erweiterungen
geordneter Tableaus: die Ordnung auf Atomen wird durch das
allgemeinere Konzept einer Auswahlfunktion ersetzt; die
Substitutivit”t, welche fžr das liften notwendig ist, kann
fžr bestimmte Varianten des Kalkžls durch eine schw”chere
Eigenschaft ersetzt werden; und eine ersten Version geordneter
Tableaus mit Theorien wird eingefžhrt. Wir zeigen die
Korrektheit und Vollst”ndigkeit der resultierenden Kalkžle.
Desweiteren berichten wir žber unsere Experimente, welche
wir mit einer prototypischen Implementierung durchgefžhrt haben,
und zeigen fžr welche Problemklassen sich geordnete Tableaus
sinnvoll einsetzen lassen.