Riassunto:
This volume contains the research papers presented at the International Con- rence on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2002) held on July 30 – August 1, 2002 in Copenhagen, Denmark, in the context of the third Federated Logic Conference (FLoC 2002). This c- ference was the continuation of international meetings on the same topic held in Lautenbach (1992), Marseille (1993), Abingdon (1994), St. Goar (1995), Ter- sini (1996), Pont-`a-Mousson (1997), Oisterwijk (1998), Saratoga Springs (1999), and St Andrews (2000). In 2001 TABLEAUX was part of IJCAR 2001 in - ena. The frame of FLoC 2002 guaranteed once again close contact to the larger Theorem Proving and Logic in Computer Science community. This was in par- cular witnessed by the talk by Matthias Baaz, jointly invited by CADE-18 and TABLEAUX 2002. Tableaux and related methods have been found to be a convenient formalism for automating deduction in various non-standard logics as well as in classical logic. This is nicely illustrated by the wide scope of logics that are covered by the papers collected in this volume: among them are linear logic, temporal - gics, various modal logics, including hybrid logic and multi-modal logics, fuzzy logics like G¨odel- andLuk asiewicz logics, various intermediate logics, quanti?ed boolean logic, and, of course, classical ?rst-order logic in various formats.
Contenuti:
Invited Papers.- Proof Analysis by Resolution.- Using Linear Logic to Reason about Sequent Systems.- Research Papers.- A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic.- Tableaux for Quantified Hybrid Logic.- Tableau-Based Automated Deduction for Duration Calculus.- Linear Time Logic, Conditioned Models, and Planning with Incomplete Knowledge.- A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic.- Modal Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks.- Tableau Calculi for the Logics of Finite k-Ary Trees.- A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition.- Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment.- Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas.- Integration of Equality Reasoning into the Disconnection Calculus.- Analytic Sequent Calculi for Abelian and ?ukasiewicz Logics.- Analytic Tableau Systems for Propositional Bimodal Logics of Knowledge and Belief.- A Confluent Theory Connection Calculus.- On Uniform Word Problems Involving Bridging Operators on Distributive Lattices.- Question Answering: From Partitions to Prolog.- A General Theorem Prover for Quantified Modal Logics.- Some New Exceptions for the Semantic Tableaux Version of the Second Incompleteness Theorem.- A New Indefinite Semantics for Hilbert’s Epsilon.- A Tableau Calculus for Combining Non-disjoint Theories.- System Descriptions Papers.- LINK: A Proof Environment Based on Proof Nets.- DCTP 1.2 — System Abstract.
Le informazioni nella sezione "Su questo libro" possono far riferimento a edizioni diverse di questo titolo.
