Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX’99 Saratoga Springs, NY, USA, June 7–11, 1999 Proceedings
Author: Neil V. Murray
Published by Springer Berlin Heidelberg
ISBN: 978-3-540-66086-6
DOI: 10.1007/3-540-48754-9

Table of Contents:

• Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions
  
• Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison
  
• DLP and FaCT
  
• Applying an
  
• KtSeqC : System Description
  
• Automated Reasoning and the Verification of Security Protocols
  
• Proof Confluent Tableau Calculi
  
• 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