Automated Reasoning with Analytic Tableaux and Related Methods International Conference, TABLEAUX'99, Saratoga Springs, NY, USA, June 7-11, 1999, Proceedings /

• Corporate Author: SpringerLink (Online service)
• Other Authors: Murray, Neil V. (Editor, http://id.loc.gov/vocabulary/relators/edt)
• Format: Electronic eBook
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.
• Edition: 1st ed. 1999.
• Series: Lecture Notes in Artificial Intelligence ; 1617
• Subjects: Artificial intelligence.; Natural language processing (Computer science).; Mathematical logic.; Artificial Intelligence.; Natural Language Processing (NLP).; Mathematical Logic and Formal Languages.

Table of Contents:

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