LEADER 05472nam 22006855 450 001 9910143644403321 005 20250730104858.0 010 $a3-540-48754-9 024 7 $a10.1007/3-540-48754-9 035 $a(CKB)1000000000211179 035 $a(SSID)ssj0000321542 035 $a(PQKBManifestationID)11937828 035 $a(PQKBTitleCode)TC0000321542 035 $a(PQKBWorkID)10280128 035 $a(PQKB)11453742 035 $a(DE-He213)978-3-540-48754-8 035 $a(MiAaPQ)EBC3072444 035 $a(MiAaPQ)EBC6485877 035 $a(PPN)155230999 035 $a(BIP)48876841 035 $a(EXLCZ)991000000000211179 100 $a20121227d1999 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Reasoning with Analytic Tableaux and Related Methods $eInternational Conference, TABLEAUX'99, Saratoga Springs, NY, USA, June 7-11, 1999, Proceedings /$fedited by Neil V. Murray 205 $a1st ed. 1999. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1999. 215 $a1 online resource (X, 334 p.) 225 1 $aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v1617 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-540-66086-0 320 $aIncludes bibliographical references and index. 327 $aExtended 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. 330 $aThisvolumecontainsaselectionofpaperspresentedattheInternationalConf- 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. 410 0$aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v1617 606 $aArtificial intelligence 606 $aNatural language processing (Computer science) 606 $aMachine theory 606 $aArtificial Intelligence 606 $aNatural Language Processing (NLP) 606 $aFormal Languages and Automata Theory 615 0$aArtificial intelligence. 615 0$aNatural language processing (Computer science) 615 0$aMachine theory. 615 14$aArtificial Intelligence. 615 24$aNatural Language Processing (NLP). 615 24$aFormal Languages and Automata Theory. 676 $a511.3 702 $aMurray$b Neil V. 712 12$aTABLEAUX '99 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910143644403321 996 $aAutomated Reasoning with Analytic Tableaux and Related Methods$92556460 997 $aUNINA