Superposition-based equality handling for analytic tableaux
From MaRDI portal
Publication:877891
DOI10.1007/S10817-006-9050-1zbMATH Open1113.68087OpenAlexW2134990618MaRDI QIDQ877891FDOQ877891
Authors: Martin Giese
Publication date: 4 May 2007
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-006-9050-1
Recommendations
Cites Work
- Resolution theorem proving
- Title not available (Why is that?)
- Solution of the Robbins problem
- Combining superposition, sorts and splitting
- Title not available (Why is that?)
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theorem proving with ordering and equality constrained clauses
- Basic paramodulation
- Paramodulation-based theorem proving
- Tableaux and related methods
- Handbook of automated reasoning. In 2 vols
- What you always wanted to know about rigid \(E\)-unification
- Automated Deduction – CADE-20
- Title not available (Why is that?)
- Theorem proving using equational matings and rigid E -unification
- Title not available (Why is that?)
- The undecidability of simultaneous rigid E-unification
- Complete sets of transformations for general E-unification
- Proving Theorems with the Modification Method
- Equality reasoning in sequent-based calculi
- Title not available (Why is that?)
- Paramodulation with built-in AC-theories and symbolic constraints
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Saturation Up to Redundancy for Tableau and Sequent Calculi
Cited In (6)
Uses Software
This page was built for publication: Superposition-based equality handling for analytic tableaux
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q877891)