Superposition-based equality handling for analytic tableaux

DOI10.1007/s10817-006-9050-1zbMath1113.68087OpenAlexW2134990618MaRDI QIDQ877891

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

Related Items (1)

Modal Tableau Systems with Blocking and Congruence Closure

Uses Software

• VAMPIRE

Cites Work

• The undecidability of simultaneous rigid E-unification
• Complete sets of transformations for general E-unification
• Paramodulation with built-in AC-theories and symbolic constraints
• Solution of the Robbins problem
• What you always wanted to know about rigid \(E\)-unification
• Theorem proving with ordering and equality constrained clauses
• Basic paramodulation
• Proving Theorems with the Modification Method
• Theorem proving using equational matings and rigid E -unification
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Saturation Up to Redundancy for Tableau and Sequent Calculi
• Automated Deduction – CADE-20
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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: Superposition-based equality handling for analytic tableaux