TABLEAUX 2003

Scientific Programme

Invited Speakers

• Vito Michele Abrusci (Università di Roma Tre, Rome, Italy)
  Non Commutative Logic: a Survey
  
• Thierry Coquand (Chalmers University of Technology, Göteborg, Sweden)
  Dynamical Method in Algebra: a Survey
  (joint speaker with Calculemus 2003)
  
  
  
• Johann Schumann (NASA Ames Research Center, Moffett Field, CA)
  Automated Theorem Proving in Generation, Verification, and Certification of Safety Critical Code

• Agata Ciabattoni (Technische Universität Wien),
  Hypersequent calculi for non classical logics.
  
• Gerhard Lakemeyer (Aachen University of Technology),
  The Situation Calculus.
  
• Jan von Plato (University of Helsinki),
  Proofs and types in constructive geometry.

Accepted Papers

Tableaux with Four Signs as a Unified Framework for Negation
Arnon Avron

A Labelled Sequent-Calculus for Observation Logic
Olivier Brunet

Bounded Lukasiewicz Logics
Agata Ciabattoni, George Metcalfe

Parallel Dialogue Games and Hypersequents for Intermediate Logics
Christian Fermüller

Simplification Rules for Constrained Formula Tableaux
Martin Giese

Tableau Calculi for Preference-based Conditional Logics
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Camilla Schwind

A General Tableau Method for Propositional Interval Temporal Logics
Valentin Goranko, Angelo Montanari, Guido Sciavicco

Universal Variables in Disconnection Tableaux
Reinhold Letz, Gernot Stenz

A Tableau Algorithm for Reasoning about Concepts and Similarity
Carten Lutz, Frank Wolter, Michael Zakharyaschev

Xpath and Modal Logics of Finite DAG's
Maarten Marx

Tableaux, Path Dissolution, and Decomposable Negation Normal Form for Knowledge Compilation
Neil V. Murray, Erik Rosenthal

A More Efficient Tableau Procedure for Simultaneous Search for Refutations and Finite Models
Nicolas Peltier

Automatic Abstraction of Equations in a Logic of Equality
Miroslav N. Velev

A Free Variable Sequent Calculus with Uniform Variable Splitting
Arild Waaler, Roger Antonsen

System Descriptions

The Tableaux Work Bench
Pietro Abate, Rajev Goré

Decision Procedures based on Second Order Logic and Modal Representations for the Propositional Cases of L Predicate Nonmonotonic Systems
Frank M. Brown

Logistica 2.0: a Technology for Implementing Automatic Deduction Systems
Frank M. Brown

Fair Constraint Merging Tableaux in Lazy Functional Programming Style
Reiner Hähnle, Niklas Sörensson

SOLAR: A Consequence Finding System SOL
Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue

CondLean: a Theorem Prover for Conditional Logics
Nicola Olivetti, Gian Luca Pozzato

Position Papers

A Tableau Formulation of Annotated Logics
Seiki Akama, Jairo Minoro Abe, Tetsuya Murai

A Parallel Implementation of a Decision Procedure for Propositional Intuitionistic Logic
Alessandro Avellone, Guido Fiorino, Ugo Moscato

Extending Stålmarck's Method to First Order Logic
Magnus Björk

Tableaux plus Constraints
Martin Giese, Reiner Hähnle

A Parallel Computation Technique for Linear Time Logic Tableaux
Carla Limongelli, Andrea Orlandini, Valentina Poggioni

Decision Procedure for a Fragment of FTL with Equality
Regimantas Pliuskevicius, Aida Pliuskeviciene

A New Form of the Semantic Tableaux Version of the Second Incompleteness Theorem
Dan E. Willard

Combining Theories Sharing Dense Orders
Calogero G. Zarba, Zohar Manna, Henny B. Sipma