A superposition oriented theorem prover

DOI10.1016/0304-3975(85)90011-8zbMath0569.68075OpenAlexW1985445827MaRDI QIDQ1060857

Laurent Fribourg

Publication date: 1985

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(85)90011-8

zbMATH Keywords

term rewritingfactoringparamodulationcompleteness of a refutation proof procedureindex-ordered resolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (3)

Problems in rewriting III ⋮ On an unsatisfiability-satisfiability prover ⋮ Theorem-proving with resolution and superposition

Cites Work

• Orderings for term-rewriting systems
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• 6th Conference on Automated Deduction, New York, USA, June 7-9, 1982
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Oriented equational clauses as a programming language
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• The Semantics of Predicate Logic as a Programming Language
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A superposition oriented theorem prover