A superposition oriented theorem prover (Q1060857)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A superposition oriented theorem prover |
scientific article |
Statements
A superposition oriented theorem prover (English)
0 references
1985
0 references
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.
0 references
completeness of a refutation proof procedure
0 references
index-ordered resolution
0 references
factoring
0 references
paramodulation
0 references
term rewriting
0 references
0 references
