Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2003, Rome, Italy, September 2003. Proceedings

V. Michele Abrusci (auth.), Marta Cialdea Mayer, Fiora Pirri (eds.)3540407871, 9783540407874

This book constitutes the refereed proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2003, held in Rome, Italy in September 2003.

The 20 revised full papers presented were carefully reviewed and selected for inclusion in the book. All current issues surrounding the mechanization of logical reasoning with tableaux and similar methods are addressed in the context of a broad variety of logic calculi.

Table of contents :
Front Matter….Pages –
Non Commutative Logic: A Survey (Abstract)….Pages 1-1
Dynamical Method in Algebra: A Survey (Abstract)….Pages 2-2
Automated Theorem Proving in Generation, Verification, and Certification of Safety Critical Code (Abstract)….Pages 3-3
Tableaux with Four Signs as a Unified Framework….Pages 4-16
A Labelled Sequent-Calculus for Observation Logic….Pages 17-31
Bounded Łukasiewicz Logics….Pages 32-47
Parallel Dialogue Games and Hypersequents for Intermediate Logics….Pages 48-64
Simplification Rules for Constrained Formula Tableaux….Pages 65-80
Tableau Calculi for Preference-Based Conditional Logics….Pages 81-101
A General Tableau Method for Propositional Interval Temporal Logics….Pages 102-116
Universal Variables in Disconnection Tableaux….Pages 117-133
A Tableau Algorithm for Reasoning about Concepts and Similarity….Pages 134-149
XPath and Modal Logics of Finite DAG‘s….Pages 150-164
Tableaux, Path Dissolution, and Decomposable Negation Normal Form for Knowledge Compilation….Pages 165-180
A More Efficient Tableaux Procedure for Simultaneous Search for Refutations and Finite Models….Pages 181-195
Automatic Abstraction of Equations in a Logic of Equality….Pages 196-213
A Free Variable Sequent Calculus with Uniform Variable Splitting….Pages 214-229
The Tableaux Work Bench….Pages 230-236
Decision Procedures for the Propositional Cases of Second Order Logic and Z Modal Logic Representations of a First Order L-Predicate Nonmonotonic Logic….Pages 237-245
Logistica 2.0: A Technology for Implementing Automatic Deduction Systems….Pages 246-251
Fair Constraint Merging Tableaux in Lazy Functional Programming Style….Pages 252-256
SOLAR: A Consequence Finding System for Advanced Reasoning….Pages 257-263
CondLean: A Theorem Prover for Conditional Logics….Pages 264-270
Back Matter….Pages –