Superposition-based equality handling for analytic tableaux

DOI10.1007/S10817-006-9050-1MaRDI QIDQ877891zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

tableau calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1950258
• scientific article; zbMATH DE number 2219496
• Hyper Tableaux with Equality
• The hyper tableaux calculus with equality and an application to finite model computation
• Superposition with equivalence reasoning and delayed clause normal form transformation.

Cites work

• scientific article; zbMATH DE number 1189096 (Why is no real title available?)
• scientific article; zbMATH DE number 1950258 (Why is no real title available?)
• scientific article; zbMATH DE number 1950261 (Why is no real title available?)
• scientific article; zbMATH DE number 1754649 (Why is no real title available?)
• scientific article; zbMATH DE number 1761415 (Why is no real title available?)
• scientific article; zbMATH DE number 1765682 (Why is no real title available?)
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 1405617 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3344563 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• Automated Deduction – CADE-20
• Basic paramodulation
• Combining superposition, sorts and splitting
• Complete sets of transformations for general E-unification
• Equality reasoning in sequent-based calculi
• Handbook of automated reasoning. In 2 vols
• Paramodulation with built-in AC-theories and symbolic constraints
• Paramodulation-based theorem proving
• Proving Theorems with the Modification Method
• Resolution theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Saturation Up to Redundancy for Tableau and Sequent Calculi
• Solution of the Robbins problem
• Tableaux and related methods
• The undecidability of simultaneous rigid E-unification
• Theorem proving using equational matings and rigid E -unification
• Theorem proving with ordering and equality constrained clauses
• What you always wanted to know about rigid \(E\)-unification

Cited in

(6)

• Adding equality to semantic tableaux
• scientific article; zbMATH DE number 1950258 (Why is no real title available?)
• scientific article; zbMATH DE number 2219496 (Why is no real title available?)
• Semantic tableaux with equality
• Hyper Tableaux with Equality
• Modal tableau systems with blocking and congruence closure

Describes a project that uses

Uses Software

• VAMPIRE

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)