THEOPOGLES - A theorem prover based on first-order polynomials and a special Knuth-Bendix procedure. THEOPOGLES is a complete theorem prover for First-Order Predicate Logic. It is based on a special Knuth-Bendix completion procedure working on First-Order Polynomials. The method does not need special AC-unification, as the N-Strategie of Hsiang, nor special overlaps with the idempotency- and nilpotence-rule, as the equational approach of Kapur and Narendran. The algorithm supports structure sharing and also linking of literals which is used for example in the Connection Graph Procedure.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Dershowitz, Nachum (ed.): Rewriting techniques and applications. 3rd international conference, RTA- 89, Chapel Hill, NC, USA, April 3-5, 1989. Proceedings (1989)
- Mueller, Juergen: THEOPOGLES - A theorem prover based on first-order polynomials and a special Knuth-Bendix procedure (1987)