A superposition oriented theorem prover
The author introduces and proves completeness of a refutation proof procedure for sets of clauses including equations and inequalities based on the rules of: index-ordered resolution and factoring and paramodulation restricted by an index-ordering and an orientation of the equations. Replacing literals (A, not B) by Boolean equations \((A=true\), \(B=false)\), the procedure has been implemented as an extension of the Knuth-Bendix algorithm for term rewriting.
completeness of a refutation proof procedure
scientific article; zbMATH DE number 3909778
scientific article