Ich habe versucht, die folgende Übung zu lösen, bin aber beim Versuch, alle kritischen Paare zu finden, festgefahren .
Ich habe folgende Fragen:
- Woher weiß ich, welches kritische Paar eine neue Regel hervorgebracht hat?
- Woher weiß ich, dass ich alle kritischen Paare gefunden habe?
Sei wobei binär ist, unär ist und eine Konstante ist.
Meine bisherige Arbeit:
(LPO 1) ist eine Variable
(LPO 2b) Es gibt keine Terme auf der rechten Seite
(LPO 2c)
- prüfen , dass ,
(LPO 1)
zu beweisen , dass (LPO 2c) wir beweisen , dass- finde so, dass s i > lpo t i i = 1 ∘ ( x , y ) > lpo x
ein. x 1 ∘ e
x ∘ y
θ { x
b. c. ( x ∘ y ) ∘ z
e ∘ x 1
x ∘ y
θ { x
Als Support-Dokument habe ich "Term Rewriting and All That" von Franz Baader und Tobias Nipkow.
EDIT1
Nach der Suche nach den kritischen Paaren habe ich die folgenden Regeln (vorausgesetzt, 2.a ist korrekt):
logic
first-order-logic
Alexandru Cimpanu
quelle
quelle
Antworten:
Bevor Sie sich mit den eigentlichen Fragen befassen, eine Bemerkung zu Ihrer bisherigen Arbeit: die linke Stornierung in 2.a. ist im Allgemeinen nicht korrekt, das kritische Paar wäre nur . Folglich erhalten Sie nicht das kritische Paar 2.b. Das Problem bei dieser Aufhebung ist, dass die Gleichung, die Sie erhalten, im Allgemeinen nicht aus den Axiomen folgt, mit denen Sie begonnen haben. Wenn Sie beispielsweise in der Sprache der Ringe arbeiten, können Sie irgendwann das kritische Paar ableiten, aber es wäre falsch, abzuleiten (was bedeuten würde, dass Sie nur haben ein triviales Modell). Kein Sound-Rewriting-Verfahren, einschließlich des von Huet, sollte diese Reduzierung zulassen.x∘(e∘z)≈x∘z 0∗x≈0∗y x≈y
Auf der anderen Seite fehlen Ihnen die kritischen Paare, die Sie erhalten, wenn Sie (in Variablen umbenannte Versionen von) oder mit allen vereinen (dh die zweite ). Die resultierenden kritischen Paare sindx∘e x∘i(x) (x∘y)∘z ∘
Für das grundlegende Abschlussverfahren:
Dieses Verfahren kann erheblich verbessert werden. Insbesondere können Sie neue Regeln verwenden, um alte zu vereinfachen (und sie möglicherweise zu verwerfen, wenn sie trivial werden, was bedeutet, dass sie von der neuen Regel subsumiert werden), und eine gute Heuristik für die Auswahl des nächsten zu untersuchenden kritischen Paares kann die drastisch reduzieren Anzahl der Regeln.
quelle