Automated Reasoning with Analytic Tableaux and Related Methods

Extended Abstracts of Invited Lectures.- Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions.- Comparison.- Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison.- DLP and FaCT.- Applying an ABox Consistency Tester to Modal Logic SAT Problems.- KtSeqC : System Description.- Abstracts of Tutorials.- Automated Reasoning and the Verification of Security Protocols.- Proof Confluent Tableau Calculi.- Contributed Research Papers.- Analytic Calculi for Projective Logics.- Merge Path Improvements for Minimal Model Hyper Tableaux.- CLDS for Propositional Intuitionistic Logic.- Intuitionisitic Tableau Extracted.- A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification.- Bounded Contraction in Systems with Linearity.- The Non-associative Lambek Calculus with Product in Polynomial Time.- Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?.- Cut-Free Display Calculi for Nominal Tense Logics.- Hilbert’s ?-Terms in Automated Theorem Proving.- Partial Functions in an Impredicative Simple Theory of Types.- A Simple Sequent System for First-Order Logic with Free Constructors.- linTAP : A Tableau Prover for Linear Logic.- A Tableau Calculus for a Temporal Logic with Temporal Connectives.- A Tableau Calculus for Pronoun Resolution.- Generating Minimal Herbrand Models Step by Step.- Tableau Calculi for Hybrid Logics.- Full First-Order Free Variable Sequents and Tableaux in Implicit Induction.- Contributed System Descriptions.- An Interactive Theorem Proving Assistant.- A Time Efficient KE Based Theorem Prover.- Strategy Parallel Use of Model Elimination with Lemmata.

Includes supplementary material: sn.pub/extras