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

by Tableaux 200 (2003 Rome, Italy); Cialdea Mayer, Marta; Pirri, Fiora

• ISBN13: 9783540407874
• ISBN10: 3540407871
• Format: Paperback
• Copyright: 2003-08-01
• Publisher: Springer Verlag

Summary

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

Short Abstracts of Invited Lectures
Non Commutative Logic: A Survey	1	(1)
V. Michele Abrusci
Dynamical Method in Algebra: A Survey	2	(1)
Thierry Coquand
Automated Theorem Proving in Generation, Verification, and Certification of Safety Critical Code	3	(1)
Johann Schumann
Research Papers
Tableaux with Four Signs as a Unified Framework	4	(13)
Arnon Avron
A Labelled Sequent-Calculus for Observation Logic	17	(15)
Olivier Brunet
Bounded Lukasiewicz Logics	32	(16)
Agata Ciabattoni
George Metcalfe
Parallel Dialogue Games and Hypersequents for Intermediate Logics	48	(17)
Christian G. Fermuller
Simplification Rules for Constrained Formula Tableaux	65	(16)
Martin Giese
Tableau Calculi for Preference-Based Conditional Logics	81	(21)
Laura Giordano
Valentina Gliozzi
Nicola Olivetti
Camilla Schwind
A General Tableau Method for Propositional Interval Temporal Logics	102	(15)
Valentin Goranko
Angelo Montanari
Guido Sciavicco
Universal Variables in Disconnection Tableaux	117	(17)
Reinhold Letz
Gernot Stenz
A Tableau Algorithm for Reasoning about Concepts and Similarity	134	(16)
Carsten Lutz
Frank Wolter
Michael Zakharyaschev
XPath and Modal Logics of Finite DAG's	150	(15)
Maarten Marx
Tableaux, Path Dissolution, and Decomposable Negation Normal Form for Knowledge Compilation	165	(16)
Neil V. Murray
Erik Rosenthal
A More Efficient Tableaux Procedure for Simultaneous Search for Refutations and Finite Models	181	(15)
Nicolas Peltier
Automatic Abstraction of Equations in a Logic of Equality	196	(18)
Miroslav N. Velev
A Free Variable Sequent Calculus with Uniform Variable Splitting	214	(16)
Arild Waaler
Roger Antonsen
System Description
The Tableaux Work Bench	230	(7)
Pietro Abate
Rajeev Gore
Decision Procedures for the Propositional Cases of Second Order Logic and Z Modal Logic Representations of a First Order L-Predicate Nonmonotonic Logic	237	(9)
Frank M. Brown
Logistica 2.0: A Technology for Implementing Automatic Deduction Systems	246	(6)
Frank M. Brown
Fair Constraint Merging Tableaux in Lazy Functional Programming Style	252	(5)
Reiner Hahnle
Niklas Sorensson
SOLAR: A Consequence Finding System for Advanced Reasoning	257	(7)
Hidetomo Nabeshima
Koji Iwanuma
Katsumi Inoue
CondLean: A Theorem Prover for Conditional Logics	264	(7)
Nicola Olivetti
Gian Luca Pozzato
Author Index	271