Inferenzsystem für Vervollständigung

(Leo Bachmair 1991, zitiert in Baader/Nipkow)

• Grundbereich: Paare (E, R) , Start: (E₀,∅), Ziel: (∅, R_n)
• Invariante: →_Rk⊆ > _A und $\approx_{{E_0}}^{}$ = $\approx_{{E_k\cup R_k}}^{}$
• Fairness: CP(R_n)⊆$\bigcup_{k}^{}$E_k

Regeln (weiter evtl. in Übung)

• deduce: (s←_Ru→_Rt) ⇒ (E, R) $\vdash$ (E∪{s $\approx$ t}, R)
• orient: (s > _At)⇒(E∪{s $\approx$ t}, R) $\vdash$ (E, R∪{s→t})
• delete: (E∪{s $\approx$ s}, R) $\vdash$ (E, R)
• simplify: (s→_R⁺u)⇒(E∪{s $\approx$ t}, R) $\vdash$ (E∪{u $\approx$ t}, R).

Korrektheit?

Warum ist einfache Vervollst. ein Spezialfall?