THEOPOGLES - A theorem prover based on first-order polynomials and a special Knuth-Bendix procedure. (English) Zbl 0628.68069

Artificial intelligence, GWAI-87, 11th Ger. Workshop, Geseke/FRG 1987, Inf.-Fachber. 152, 241-250 (1987).
[For the entire collection see Zbl 0623.00020.]
This paper introduces a complete theorem prover and its implementation. The algorithm supports structure sharing and linking of literals. It overcomes problems as the need of special unification and complicated orderings, and it reduces the complexity of search.
Reviewer: E.Melis


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)


Zbl 0623.00020