Hyper tableaux

DOI10.1007/3-540-61630-6_1zbMath1427.03031OpenAlexW2912282119MaRDI QIDQ5235250

Peter Baumgartner, Ulrich Furbach, Ilkka Niemelä

Publication date: 8 October 2019

Published in: Logics in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61630-6_1

zbMATH Keywords

universal variableproof procedureground instanceopen branchrigid variable

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (24)

Combining event calculus and description logic reasoning via logic programming ⋮ Representing ontologies using description logics, description graphs, and rules ⋮ The model evolution calculus as a first-order DPLL method ⋮ Craig interpolation with clausal first-order tableaux ⋮ On First-Order Model-Based Reasoning ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ Hyperresolution for guarded formulae ⋮ Tableaux for diagnosis applications ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ A framework for using knowledge in tableau proofs ⋮ Individual Reuse in Description Logic Reasoning ⋮ Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) ⋮ Theorem proving techniques for view deletion in databases ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ Magic sets for disjunctive Datalog programs ⋮ On the equivalence of the static and disjunctive well-founded semantics and its computation ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Lemma matching for a PTTP-based top-down theorem prover ⋮ The proof complexity of analytic and clausal tableaux ⋮ EXPtime tableaux for ALC ⋮ Possible models computation and revision -- a practical approach ⋮ Efficient model generation through compilation. ⋮ Set of support, demodulation, paramodulation: a historical perspective

Uses Software

• TPTP
• SATCHMO
• 3TAP
• HARP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification theory
• Controlled integration of the cut rule into connection tableau calculi
• SATCHMORE: SATCHMO with RElevancy
• lean\(T^ AP\): Lean tableau-based deduction
• A fixpoint semantics for disjunctive logic programs
• The disconnection method
• A tableau calculus for minimal model reasoning
• The TPTP problem library

This page was built for publication: Hyper tableaux