Automated reasoning with analytic tableaux and related methods

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