Automated Reasoning with Analytic Tableaux and Related Methods

Inhaltsverzeichnis

• Invited Talks.
• Query Processing in Peer-to-Peer Systems: An Epistemic Logic Approach.
• Description Logics in Ontology Applications.
• Automated Reasoning in the Context of the Semantic Web.
• Formal Versus Rigorous Mathematics: How to Get Your Papers Published.
• Research Papers.
• Consistency of Variable Splitting in Free Variable Systems of First-Order Logic.
• On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic.
• A Tableau-Based Decision Procedure for Right Propositional Neighborhood Logic.
• Cyclic Proofs for First-Order Logic with Inductive Definitions.
• A Tableau-Based Decision Procedure for a Fragment of Graph Theory Involving Reachability and Acyclicity.
• Embedding Static Analysis into Tableaux and Sequent Based Frameworks.
• A Calculus for Type Predicates and Type Coercion.
• A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics.
• Comparing Instance Generation Methods for Automated Reasoning.
• An Order-Sorted Quantified Modal Logic for Meta-ontology.
• A Redundancy Analysis of Sequent Proofs.
• A Tableau Algorithm for Description Logics with Concrete Domains and GCIs.
• The Space Efficiency of OSHL.
• Efficient Query Processing with Compiled Knowledge Bases.
• Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic.
• Automatic ‘Descente Infinie’ Induction Reasoning.
• A Decision Procedure for the Alternation-Free Two-Way Modal ?-Calculus.
• On the Partial Respects in Which a Real Valued Arithmetic System Can Verify Its Tableaux Consistency.
• System Descriptions.
• Pdk: The System and Its Language.
• Proof Output and Transformation for Disconnection Tableaux.
• LoTREC: Logical Tableaux Research Engineering Companion.
• A Tableau-Based Explainer for DL Subsumption.
• CondLean 3.0: Improving CondLean for Stronger Conditional Logics.
• The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic.
• Unit Propagation in a Tableau Framework.