Blick ins Buch

Automated Reasoning with Analytic Tableaux and Related Methods

International Conference, TABLEAUX 2000 St Andrews, Scotland, UK, July 3-7, 2000 Proceedings

Roy Dyckhoff (Herausgeber)

Buch | Softcover

X, 440 Seiten

2000 | 2000
Springer Berlin (Verlag)
978-3-540-67697-3 (ISBN)

Lese- und Medienproben

Inhaltsverzeichnis (PDF)

Artikel merken

This volume contains the main papers presented at the International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000) held on July 3 7, 2000 in St Andrews, Scotland. This conference succeeded other meetings on the same topic held in Lautenbach (1992), Marseille (1993), Abingdon (1994), St Goar (1995), Terrasini (1996), Pont-` a-Mousson (1997), Oisterwijk (1998) and Saratoga Springs (1999). Tableaux and related methods, such as Gentzen calculi, are convenient and e?ective for automating deduction not just in classical logic but also in various non-standard logics. Examples taken from this meeting alone include temporal, description, non-monotonic, tense, modal, epistemic, fuzzy and intuitionistic - gics. Areas of application include veri?cation of software and computer systems, deductive databases, knowledge representation and system diagnosis. The c- ference brought together researchers interested in all aspects theoretical fo- dations, implementation techniques, systems development, experimental com- rison and applications of the automation of reasoning by means of tableaux or related methods.

Invited Lectures.- Tableau Algorithms for Description Logics.- Modality and Databases.- Local Symmetries in Propositional Logic.- Comparison.- Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison.- Consistency Testing: The RACE Experience.- Benchmark Analysis with FaCT.- MSPASS: Modal Reasoning by Translation and First-Order Resolution.- TANCS-2000 Results for DLP.- Evaluating *SAT on TANCS 2000 Benchmarks.- Research Papers.- A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations.- A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus.- An Analytic Calculus for Quantified Propositional Gödel Logic.- A Tableau Method for Inconsistency-Adaptive Logics.- A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning.- Hypertableau and Path-Hypertableau Calculi for some Families of Intermediate Logics.- Variants of First-Order Modal Logics.- Complexity of Simple Dependent Bimodal Logics.- Properties of Embeddings from Int to S4.- Term-Modal Logics.- A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics.- Dual Intuitionistic Logic Revisited.- Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions.- Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints.- Matrix-Based Inductive Theorem Proving.- Monotonic Preorders for Free Variable Tableaux.- The Mosaic Method for Temporal Logics.- Sequent-Like Tableau Systems with the Analytic Superformula Property for the Modal Logics KB, KDB, K5, KD5.- A Tableau Calculus for Equilibrium Entailment.- Towards Tableau-Based Decision Procedures for Non-Well-Founded Fragments of Set Theory.- Tableau Calculus for Only Knowing and Knowing At Most.- A Tableau-Like RepresentationFramework for Efficient Proof Reconstruction.- The Semantic Tableaux Version of the Second Incompleteness Theorem Extends Almost to Robinson's Arithmetic Q.- System Descriptions.- Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO.- E-SETHEO: An Automated3 Theorem Prover.

Erscheint lt. Verlag	21.6.2000
Reihe/Serie	Lecture Notes in Artificial Intelligence
Reihe/Serie	Lecture Notes in Computer Science
Zusatzinfo	X, 440 p.
Verlagsort	Berlin
Sprache	englisch
Maße	155 x 235 mm
Gewicht	635 g
Themenwelt	Informatik ► Theorie / Studium ► Compilerbau
Themenwelt	Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik
Schlagworte	AI logics • Automat • automated deduction • automated reasoning • Formal Verification • Logic Reason Calculi • Mathematical Logics • Modal Logics • Tableaux Methods • theorem proving
ISBN-10	3-540-67697-X / 354067697X
ISBN-13	978-3-540-67697-3 / 9783540676973
Zustand	Neuware