| 9:00 am | Invited talk: Johann Schumann (NASA Ames Research Center, Moffett Field, CA) | |||
| 10:00 | Arnon Avron. Tableaux with Four Signs as a Unified Framework for Negation | |||
| 10:30-11:00 | | |||
| 11:00-11:30 | Olivier Bruent. A Labelled Sequent-Calculus for Observation Logic | |||
| 11:30-12:00 | Agata Ciabattoni, George Metcalfe. Bounded Lukasiewicz Logics | |||
| 12:00-12:30 | Christian Fermüller. Parallel Dialogue Games and Hypersequents for Intermediate Logics | |||
| 12:30-14:00 | | |||
| 14:00-14:30 | Martin Giese Simplification Rules for Constrained Formula Tableaux | |||
| 14:30-15:30 |
| |||
| 15:30-16:00 | | |||
| 16:00-18:00 | TUTORIALS (continued) |
| 9:00 am | Invited talk: Vito Michele Abrusci (Università di Roma Tre, Rome, Italy) | |
| 10:00 | Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Camilla Schwind. Tableau Calculi for Preference-Based Conditional Logics | |
| 10:30-11:00 | | |
| 11:00 | Valentin Goranko, Angelo Montanari, Guido Sciavicco. A General Tableau Method for Propositional Interval Temporal Logics | |
| 11:30 | Reinhold Letz, Gernot Stenz. Universal Variables in Disconnection Tableaux | |
| 12:00 | Carten Lutz, Frank Wolter, Michael Zakharyaschev. A Tableau Algorithm for Reasoning about Concepts and Similarity | |
| 12:30-14:00 | | |
| 14:00 | Maarten Marx. Xpath and Modal Logics of Finite DAG's | |
| | ||
| 14:30 | Seiki Akama, Jairo Minoro Abe, Tetsuya Murai. A Tableau Formulation of Annotated Logics | |
| 14:50 | Alessandro Avellone, Guido Fiorino, Ugo Moscato. A Parallel Implementation of a Decision Procedure for Propositional Intuitionistic Logic | |
| 15:10 | Magnus Björk. Extending Stålmarck's Method to First Order Logic | |
| 15:30-16:00 | | |
| 16:00 | Martin Giese, Reiner Hähnle. Tableaux + Constraints | |
| 16:40 | Carla Limongelli, Andrea Orlandini, Valentina Poggioni. A Parallel Computation Technique for Linear Time Logic Tableaux | |
| 17:00 | Regimantas Pliuskevicius, Aida Pliuskeviciene. Decision Procedure for a Fragment of FTL with Equality | |
| 17:20 | Dan E. Willard. A New Form of the Semantic Tableaux Version of the Second Incompleteness Theorem | |
| 17:40 | Calogero G. Zarba, Zohar Manna, Henny B. Sipma. Combining Theories Sharing Dense Orders |
| 9:00 am | Invited talk: Thierry Coquand (Chalmers University of Technology, Göteborg, Sweden) |
| 10:00 | Neil V. Murray, Erik Rosenthal. Tableaux, Path Dissolution, and Decomposable Negation Normal Form for Knowledge Compilation |
| 10:30-11:00 | |
| 11:00 | Nicolas Peltier. A More Efficient Tableau Procedure for Simultaneous Search for Refutations and Finite Models |
| 11:30 | Miroslav N. Velev. Automatic Abstraction of Equations in a Logic of Equality |
| 12:00 | Arild Waaler, Roger Antonsen. A Free Variable Sequent Calculus with Uniform Variable Splitting |
| 12:30-14:00 | |
| 14:00 | Villa Adriana and Villa d'Este Tivoli (about 30 Km from Rome) AND SOCIAL DINNER |
| | |||||||
| 9:00 | Pietro Abate, Rajev Goré. The Tableaux Work Bench | ||||||
| 9:30 | Frank M. Brown. Decision Procedures for the Propositional Cases of Second Order Logic and Z Modal Logic Representations of a First Order L-Predicate Nonmonotonic Logic | ||||||
| 10:00 | Reiner Hähnle, Niklas Sörensson. Fair Constraint Merging Tableaux in Lazy Functional Programming Style | ||||||
| 10:30-11:00 | | ||||||
| 11:00 | Frank M. Brown. Logistica 2.0: A Technology for Implementing Automatic Deduction Systems | ||||||
| 11:30 | Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue. SOLAR: A Consequence Finding System for Advanced Reasoning | ||||||
| 12:00 | Nicola Olivetti, Gian Luca Pozzato. CondLean: a Theorem Prover for Conditional Logics | ||||||
| 12:30-14:00 | | ||||||
| 14:00 | PANEL DISCUSSION ON OPEN CHALLENGES OF COMPUTERIZED MATHEMATICS Joint with Calculemus and TPHOLs 2003 15:30-16:00 |
| 16:00 |
PANEL DISCUSSION (continued) 17:00 |
|