Automated Reasoning with Analytic Tableaux and Related Methods

Invited Papers.- Proof Analysis by Resolution.- Using Linear Logic to Reason about Sequent Systems.- Research Papers.- A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic.- Tableaux for Quantified Hybrid Logic.- Tableau-Based Automated Deduction for Duration Calculus.- Linear Time Logic, Conditioned Models, and Planning with Incomplete Knowledge.- A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic.- Modal Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks.- Tableau Calculi for the Logics of Finite k-Ary Trees.- A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition.- Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment.- Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas.- Integration of Equality Reasoning into the Disconnection Calculus.- Analytic Sequent Calculi for Abelian and ?ukasiewicz Logics.- Analytic Tableau Systems for Propositional Bimodal Logics of Knowledge and Belief.- A Confluent Theory Connection Calculus.- On Uniform Word Problems Involving Bridging Operators on Distributive Lattices.- Question Answering: From Partitions to Prolog.- A General Theorem Prover for Quantified Modal Logics.- Some New Exceptions for the Semantic Tableaux Version of the Second Incompleteness Theorem.- A New Indefinite Semantics for Hilbert’s Epsilon.- A Tableau Calculus for Combining Non-disjoint Theories.- System Descriptions Papers.- LINK: A Proof Environment Based on Proof Nets.- DCTP 1.2 — System Abstract.

Includes supplementary material: sn.pub/extras