+612 9045 4394
Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, Tableaux'99, Saratoga Springs, Ny, Usa, June 7-11, 1999, Proceedings - Neil V. Murray

Automated Reasoning with Analytic Tableaux and Related Methods

International Conference, Tableaux'99, Saratoga Springs, Ny, Usa, June 7-11, 1999, Proceedings

By: Neil V. Murray (Editor)


Published: 26th May 1999
Ships: 15 business days
15 business days
or 4 easy payments of $31.26 with Learn more

ThisvolumecontainsaselectionofpaperspresentedattheInternationalConf- ence on Analytic Tableaux and Related Methods (TABLEAUX'99) held on June 7-11, 1999 at the Inn at Saratoga, Saratoga Springs, NY, USA. This conference was the continuation of international meetings on Theorem Proving with A- lytic Tableaux and Related Methods held in Lautenbach near Karlsruhe (1992), Marseille (1993), Abingdon near Oxford (1994), St. Goar near Koblenz (1995), Terrasini near Palermo (1996), Pont-` a-Mousson near Nancy (1997), and Oist- wijk near Tilburg (1998). TABLEAUX'99 marks the ?rst time the conference has been held in North America. Tableau and related methods have been found to be convenient and e?ective for automating deduction in various non-standard logics as well as in classical logic. Examples taken from this meeting alone include temporal, description, tense, quantum, modal, projective, hybrid, intuitionistic, and linear logics. - eas of application include veri?cation of software and computer systems, ded- tive databases, knowledge representation and its required inference engines, and system diagnosis. The conference brought together researchers interested in all aspects - theoretical foundations, implementation techniques, systems devel- ment and applications - of the mechanization of reasoning with tableaux and related methods.

Extended Abstracts of Invited Lectures
Microprocessor Verification Using Efficient Decision Procedures for a Logic of `zEquality with Uninterpreted Functionsp. 1
Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparisonp. 14
DLP and FaCTp. 19
Applying an <$$$> ABox Consistency Tester to Modal Logic SAT Problemsp. 24
KtSeqC: System Descriptionp. 29
Abstracts of Tutorials
Automated Reasoning and the Verification of Security Protocolsp. 32
Proof Confluent Tableau Calculip. 34
Contributed Research Papers
Analytic Calculi for Projective Logicsp. 36
Merge Path Improvements for Minimal Model Hyper Tableauxp. 51
CLDS for Propositional Intuitionistic Logicp. 66
Intuitionisitic Tableau Extractedp. 82
A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantificationp. 97
Bounded Contraction in Systems with Linearityp. 113
The Non-associative Lambek Calculus with Product in Polynomial Timep. 128
Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?p. 140
Cut-Free Display Calculi for Nominal Tense Logicsp. 155
Hilbert's Epsilon-Terms in Automated Theorem Provingp. 171
Partial Functions in an Impredicative Simple Theory of Typesp. 186
A Simple Sequent System for First-Order Logic with Free Constructorsp. 202
linTAP: A Tableau Prover for Linear Logicp. 217
A Tableau Calculus for a Temporal Logic with Temporal Connectivesp. 232
A Tableaux Calculus for Pronoun Resolutionp. 247
Generating Minimal Herbrand Models Step by Stepp. 263
Tableau Calculi for Hybrid Logicsp. 278
Full First-Order Free Variable Sequents and Tableaux in Implicit Inductionp. 293
Contributed System Descriptions
An Interactive Theorem Proving Assistantp. 308
A Time Efficient KE Based Theorem Proverp. 313
Strategy Parallel Use of Model Elimination with Lemmata - System Abstract -p. 319
Author Indexp. 325
Table of Contents provided by Publisher. All Rights Reserved.

ISBN: 9783540660866
ISBN-10: 3540660860
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 334
Published: 26th May 1999
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 1.83
Weight (kg): 0.48