Inferenzsystem für Vervollständigung

(Leo Bachmair 1991, zitiert in Baader/Nipkow)

Regeln (weiter evtl. in Übung)

Korrektheit?

Warum ist einfache Vervollst. ein Spezialfall?