Mueller, Juergen 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 MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Citations:Zbl 0623.00020 Software:THEOPOGLES PDFBibTeX XML