TABLEAUX program

Sessions take place in auditorium 3 unless otherwise indicated.

Monday July 29th

Monday's program is also available side by side with other meetings.

19:00-21:00  City Hall reception (joint with CADE, CAV, ICLP)
Room: City Hall

Tuesday July 30th

Tuesday's program is also available with abstracts or side by side with other meetings.

11:30-12:30  Invited talk (joint with CADE)

11:30  Matthias Baaz, Vienna U of Techn., Austria
Invited talk: Proof analysis by resolution

12:30-14:00  Lunch

14:00-15:30  Session 1

14:00  Anatoli Degtyarev, Michael Fisher, and Boris Konev; U Liverpool, UK
A simplified clausal resolution procedure for propositional linear-time temporal logic
14:30  Nathalie Chetcuti-Sperandio, IRIT Toulouse, France
Tableau-based automated deduction for duration calculus
15:00  Marta Cialdea Mayer and Carla Limongelli, U Rome III, Italy
Linear time logic, conditioned models and planning with incomplete knowledge

15:30-16:00  Refreshments

16:00-17:30  Session 2

16:00  Reinhold Letz and Gernot Stenz, Techn. U of Munich, Germany
Integration of equality reasoning into the disconnection calculus
16:30  Viorica Sofronie-Stokkermans, MPI Saarbrücken, Germany
Deciding uniform word problems involving bridging operators on bounded distributive lattices
17:00  Uwe Petermann, Leipzig U of Applied Sciences, Germany
A confluent theory connection calculus

Wednesday July 31st

Wednesday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 3

09:00  Dale Miller and Elaine Pimentel, Penn State U, USA
Invited talk: Using linear logic to reason about sequent systems
10:00  Martin Giese, Karlsruhe U, Germany
A model generation style completeness proof for constraint tableaux with superposition

10:30-11:00  Refreshments

11:00-12:30  Session 4

11:00  Thomas Eiter, Volker Klotz, Hans Tompits, and Stefan Woltran; Vienna U of Techn., Austria
Modal nonmonotonic logics revisited: Efficient encodings for the basic reasoning tasks
11:30  Reinhold Letz, Techn. U of Munich, Germany
Lemma and model caching in decision procedures for quantified boolean formulas
12:00  Balder ten Cate, U Amsterdam, The Netherlands and Chung-chieh Shan, Harvard U, USA
Question answering: from partitions to prolog

12:30-14:00  Lunch

14:00-15:30  Session 5

14:00  George Metcalfe, King's College London, UK; Nicola Olivetti, U Turin, Italy; and Dov Gabbay, King's College London, UK
Analytic sequent calculi for abelian and Lukasiewicz logics
14:30  Matthias Baaz and Agata Ciabattoni, Vienna U of Techn., Austria
A Schütte-Tait style cut-elimination proof for first-order Gödel logic
15:00  Mauro Ferrari, U Milan, Italy; Camillo Fiorentini, U Milan, Italy; and Guido Fiorino, Varese U, Italy
Tableau calculi for the logics of finite k-ary trees

15:30-16:00  Refreshments

16:00-17:30  Session 6

16:00  Calogero G. Zarba, Stanford U, USA
A tableau calculus for combining non-disjoint theories
16:30  Gernot Stenz, Techn. U of Munich, Germany
System description: DCTP 1.2
17:00  Luc Habert, Jean-Marc Notin, and Didier Galmiche; LORIA Nancy, France
System description: LINK: a proof environment based on proof nets

17:30-18:30  TABLEAUX Business Meeting

19:30-22:00  Conference dinner (joint with ICLP)
Room: Restaurant Luftkastellet

19:30  Banquet
20:30  Veronica Dahl, Simon Fraser U, Canada (Banquet speaker)

Thursday August 1st

Thursday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 7

09:00  Patrick Blackburn, LORIA Nancy, France and Maarten Marx, U Amsterdam, The Netherlands
Tableaux for quantified hybrid logic
09:30  Virginie Thion, U Paris XI (Paris-Sud), France; Serenella Cerrito, U Paris XI (Paris-Sud), France; and Marta Cialdea Mayer, U Rome III, Italy
A general theorem prover for quantified modal logics
10:00  Linh Anh Nguyen, Warsaw U, Poland
Analytic tableau systems for propositional bimodal logics of knowledge and belief

10:30-11:00  Refreshments

11:00-12:30  Session 8

11:00  Jan Hladik, Dresden U of Techn., Germany
Implementation and optimization of a tableau algorithm for the guarded fragment
11:30  Claus-Peter Wirth, Saarland U, Germany
A new indefinite semantics for Hilbert's epsilon
12:00  Dan E. Willard, State U of New York-Albany, USA
Some new exceptions for the semantic tableaux version of the second incompletness theorem

12:30-14:00  Lunch

14:00-15:40  Session 9: Position papers

14:00  Reiner Hähnle, Chalmers U of Techn., Sweden; Neil V. Murray, State U of New York-Albany, USA; and Erik Rosenthal, U New Haven, USA
Position paper: Unit preference for ordered resolution and for connection graph resolution
14:20  Georg Moser, Vienna U of Techn., Austria
Position paper: Epsilon, delta, and speed-ups
14:40  James Harland, RMIT U, Australia
Position paper: Search calculi for classical and intuitionistic logic
15:00  Guido Fiorino, Varese U, Italy
Position paper: Improving the treatment of negation in propositional Dummett logic
15:20  Breanndán Ó Nualláin, U Amsterdam, The Netherlands
Position paper: Constraint tableaux

15:40-16:00  Refreshments

16:10-17:30  Session 10: Position papers

16:10  Frank M. Brown, U Kansas, USA
Position paper: A tableaux based system for propositional nonmonotonic logics
16:30  Jens Happe, Simon Fraser U, Canada
Position paper: Free-variable tableaux for efficient deduction in K
16:50  Regimantas Pliuskevicius, Inst. of Mathematics and Informatics, Vilnius, Lithuania
Position paper: A parametrical similarity saturation based decision procedure for a fragment of FTL
17:10  Norbert Preining, Vienna U of Techn., Austria
Position paper: Proof theory and proof systems for projective and affine geometry