FLoC '02 - TABLEAUX program

TABLEAUX program

Sessions take place in auditorium 3 unless otherwise indicated.

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'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'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

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'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