Superposition with equivalence reasoning and delayed clause normal form transformation
From MaRDI portal
Publication:2486577
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
Automated theorem provingSet theoryRewritingSuperpositionFirst-order logicDeductionClause-normal-form transformationLogical equivalenceParamodulation
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
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