Superposition-based equality handling for analytic tableaux

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

• 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.

zbMATH Keywords

tableau calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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)

• Adding equality to semantic tableaux
• Title not available (Why is that?)
• Title not available (Why is that?)
• Semantic tableaux with equality
• Hyper Tableaux with Equality
• Modal tableau systems with blocking and congruence closure

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)