Hyper tableau -- the next generation

DOI10.1007/3-540-69778-0_14MaRDI QIDQ3838803zbMATH OpenFDO

Authors Peter Baumgartner

Publication date 19 April 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-69778-0_14

zbMATH Keywords

automated reasoninghyper tableau calculusmodel extraction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

The paper presents an improvement of hyper tableau calculus which removes the need to blindly guess ground instantiation for certain clauses. This guessing is replaced by a unification-driven technique. The hyper tableau is different from hyperresolution and relates with analytic resolution. Hyper-type inferences restrict the possible inferences. This fact makes the hyper tableau method a decision method for the Bernays-Schoenfinkel class. For the entire collection see [Zbl 0888.00018].

Recommendations

• Hyper tableaux
• HyperS tableaux -- heuristic hyper tableaux
• Constrained hyper tableaux
• The hyper tableaux calculus with equality and an application to finite model computation
• scientific article; zbMATH DE number 2219496

Cited in

(21)

• Hyperresolution for guarded formulae
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Set of support, demodulation, paramodulation: a historical perspective
• SCL(EQ): SCL for first-order logic with equality
• SCL clause learning from simple models
• The model evolution calculus as a first-order DPLL method
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• Semantically-guided goal-sensitive reasoning: model representation
• The hyper tableaux calculus with equality and an application to finite model computation
• Merge path improvements for minimal model hyper tableaux
• scientific article; zbMATH DE number 1543303 (Why is no real title available?)
• Constrained hyper tableaux
• Hyper tableaux
• Automated Deduction – CADE-20
• HyperS tableaux -- heuristic hyper tableaux
• Theorem proving techniques for view deletion in databases
• SCL(EQ): SCL for first-order logic with equality
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Exploring partial models with SCL
• The disconnection tableau calculus
• Superposition-based equality handling for analytic tableaux

This page was built for publication: Hyper tableau -- the next generation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3838803)