Automated reasoning with analytic tableaux and related methods

InhaltsverzeichnisInvited Talks.Nonmonotonic Description Logics – Requirements, Theory, and Implementations.Our Quest for the Holy Grail of Agent Verification.An Abstract Framework for Satisfiability Modulo Theories.Research Papers.Axiom Pinpointing in General Tableaux.Proof Theory for First Order ? ukasiewicz Logic.A Tableau Method for Public Announcement Logics.Bounded Model Checking with Description Logic Reasoning.Tableau Systems for Logics of Subinterval Structures over Dense Orderings.A Cut-Free Sequent Calculus for Bi-intuitionistic Logic.Tableaux with Dynamic Filtration for Layered Modal Logics.The Neighbourhood of S0.9 and S1.EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies.Tree-Sequent Methods for Subintuitionistic Predicate Logics.A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation.Updating Reduced Implicate Tries.A Bottom-Up Approach to Clausal Tableaux.Differential Dynamic Logic for Verifying Parametric Hybrid Systems.System Descriptions.Improvements to the Tableau Prover PITP.KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning.