A superposition oriented theorem prover
type: Item
instance of: scholarly article
title: A superposition oriented theorem prover
zbMATH Open document ID: 0569.68075
DOI: 10.1016/0304-3975(85)90011-8
author: Laurent Fribourg
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 3909778
zbMATH Keywords: completeness of a refutation proof procedure
zbMATH Keywords: index-ordered resolution
zbMATH Keywords: factoring
zbMATH Keywords: paramodulation
zbMATH Keywords: term rewriting
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90011-8
OpenAlex ID: W1985445827
cites work: Orderings for term-rewriting systems
cites work: The Semantics of Predicate Logic as a Programming Language
cites work: Q3338216
cites work: Oriented equational clauses as a programming language
cites work: Q3336735
cites work: Q3880309
cites work: Q3674088
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Q3659124
cites work: Q5581665
cites work: Q4139711
cites work: Q3338214
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: 6th Conference on Automated Deduction, New York, USA, June 7-9, 1982
cites work: Q5624683
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: A Unification Algorithm for Associative-Commutative Functions
cites work: Q5507984
cites work: The Concept of Demodulation in Theorem Proving
description: scientific article; zbMATH DE number 3909778