scientific article
From MaRDI portal
Publication:2751356
zbMath1005.03013MaRDI QIDQ2751356
Matthias Baaz, Alexander Leitsch, Uwe Egly
Publication date: 27 August 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)
Related Items
Semantic forgetting in expressive description logics, Quantifier simplification by unification in SMT, The problem of \(\Pi_{2}\)-cut-introduction, Canonical signed calculi with multi-ary quantifiers, Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments, Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction), Combining decision procedures by (model-)equality propagation, Deciding expressive description logics in the framework of resolution, Reasoning in description logics by a reduction to disjunctive datalog, Translation of resolution proofs into short first-order proofs without choice axioms, Proof Transformations and Structural Invariance, Bounded treewidth as a key to tractability of knowledge representation and reasoning, Canonical Signed Calculi, Non-deterministic Matrices and Cut-Elimination, Scalable fine-grained proofs for formula processing, On Stronger Calculi for QBFs, Combinations of Theories for Decidable Fragments of First-Order Logic
