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

Anything in here will be replaced on browsers that support the canvas element