Superposition with equivalence reasoning and delayed clause normal form transformation

DOI10.1016/j.ic.2004.10.010zbMath1081.68092OpenAlexW1980214308MaRDI QIDQ2486577

Harald Ganzinger, Jürgen Stuber

Publication date: 5 August 2005

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00071750/file/RR-4835.pdf

zbMATH Keywords

Automated theorem provingSet theoryRewritingSuperpositionFirst-order logicDeductionClause-normal-form transformationLogical equivalenceParamodulation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Superposition for higher-order logic, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, From Search to Computation: Redundancy Criteria and Simplification at Work, Superposition with lambdas, Superposition with lambdas, Superposition with first-class booleans and inprocessing clausification, Superposition for full higher-order logic, A comprehensive framework for saturation theorem proving

Uses Software

• VAMPIRE
• Saturate

Cites Work

• Completely non-clausal theorem proving
• Gentzen-type systems, resolution and tableaux
• Theorem proving modulo
• Theorem proving with ordering and equality constrained clauses
• Basic paramodulation
• A Deductive Approach to Program Synthesis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item