TUESDAY, JUNE 8, 1999

Session I	Chair: (TBA)
9:00 - 10:00am:	Invited Talk: Randal Bryant (CMU), Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions.
10:00 - 10:20:	Break
Session II	Chair: (TBA)
10:20 - 10:40am:	Bernhard Beckert, Depth-first Proof Search without Backtracking for Free Variable Semantic Tableaux.
10:40 - 11:00am:	Alessandro Avellone, Marco Benini, and Ugo Moscato, Tactics for Translation of Tableau in Natural Deduction.
11:00 - 11:30am:	Peter Baumgartner, Joe Horton, and Bruce Spencer, Merge Path Improvements for Minimal Model Hyper Tableaux.
11:30am - 12:00pm:	Jean Goubault-Larrecq, A Simple Sequent System for First-Order Logic with Free Constructors.
12:00 - 1:30pm:	LUNCH
Session III	Chair: (TBA)
1:30 - 2:00pm:	Wolfgang May, A Tableau Calculus for a Temporal Logic with Temporal Connectives.
2:00 - 2:30pm:	Ulrich Endriss, An Interactive Theorem Proving Assistant.
2:30 - 3:00pm:	Ulrich Endriss, A Time Efficient KE Based Theorem Prover.
3:00 - 3:30pm:	Break
Session IV	Chair: (TBA)
3:30 - 4:00pm:	Andreas Wolf and Joachim Draeger, Strategy Parallel Use of Model Elimination with Lemmata - System Abstract -.
4:00 - 5:00pm:	COMPARISON of Theorem Provers for Non Classical (Modal) Systems.
4:00 - 4:15pm:	Fabio Massacci, Design and Results of the Tableaux-99 Non-Classical (Modal) Systems Comparison.
4:15 - 4:30pm:	Peter F. Patel-Schneider and Ian Horrocks, DLP and FaCT.
4:30 - 4:45pm:	Volker Haarslev and Ralf Moeller, Applying an ALC ABox Consistency Tester to Modal Logic SAT Problems.
4:45 - 5:00pm:	Vijay Boyapati and Rajeev Goré, KtSeqC: System Description.

WEDNESDAY, JUNE 9, 1999

Session V	Chair: (TBA)
9:00 - 10:00am:	Invited Talk: David S. Warren (SUNY Stony Brook), The XSB tabled logic programming system.
10:00 - 10:20am:	Break
Session VI	Chair: (TBA)
10:20 - 10:40am:	Uwe Egly and Hans Tompits, Gentzen-Like Methods in Quantum Logic.
10:40 - 11:00am:	Shigeki Hagihara and Naoki Yonezaki, Unification-based Proof Method for Modal Logic with Well-founded Frames.
11:00 - 11:30am:	Martin Giese and Wolfgang Ahrendt, Hilbert's Epsilon-Terms in Automated Theorem Proving.
11:30am - 12:00pm:	Christof Monz and Maarten de Rijke, A Tableaux Calculus for Pronoun Resolution.
12:00 - 1:30pm:	LUNCH
Session VII	Chair: (TBA)
1:30 - 2:00pm:	Matthias Baaz & Christian Fermüller, Analytic Calculi for Projective Logics.
2:00 - 2:30pm:	Miroslava Tzakova, Tableau Calculi for Hybrid Logics.
2:30 - 3:00pm:	Claus-Peter Wirth, Full First-Order Free Variable Sequents and Tableaux in Implicit Induction.
3:00 - 3:30pm:	Break
Session VIII	Chair: (TBA)
3:30 - 4:00pm:	Krysia Broda and Dov Gabbay, CLDS for Propositional Intuitionistic Logic.
4:00pm - 4:30pm:	James Caldwell, Intuitionisitic Tableau Extracted.
4:30pm - 4:50pm:	Claus Zinn, COLOSSEUM \- An Automated Theorem Prover for Intuitionistic Predicate Logic based on Dialogue Games.
4:50pm - 5:10pm:	Karl-Michael Schneider, An Application of Labelled Tableaux to Parsing.
6:30 - 9:00pm:	CONFERENCE BANQUET at the Canfield Casino (Dinner Speaker: City of Schenectady Corporation Counsel Michael T. Brockbank)

THURSDAY, JUNE 10, 1999

Tutorial Sessions
9:00am - 10:20am:	Tutorial 1: Fabio Massacci, Automated Reasoning and the Verification of Security Protocols.
or	Tutorial 2: Reiner Hähnle and Bernhard Beckert, Proof Confluent Tableau Calculi.
10:20 - 10:40am:	Break
10:40am - 12:00pm:	Tutorial 1: Fabio Massacci, Automated Reasoning and the Verification of Security Protocols.
or	Tutorial 2: Reiner Hähnle and Bernhard Beckert, Proof Confluent Tableau Calculi.
12:00 - 1:30pm:	LUNCH
Session IX	Chair: (TBA)
1:30 - 2:00pm:	Stéphane Demri, Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?
2:00 - 2:30pm:	Stéphane Demri and Rajeev Goré, Cut-free Display Calculi for Nominal Tense Logics.
2:30 - 3:00pm:	Break
Session X	Chair: (TBA)
3:00 - 3:30pm:	Domenico Cantone and Calogero G. Zarba, A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification.
3:30 - 4:00pm:	Paul C. Gilmore, Partial Functions in an Impredicative Simple Theory of Types.
4:15 - 5:45pm:	Walking Tour

FRIDAY, JUNE 11, 1999

Session XI	Chair: (TBA)
9:00 - 9:30am:	Agata Ciabattoni, Bounded Contraction in Systems with Linearity.
9:30 - 10:00am:	Heiko Mantel and Jens Otten, linTAP: A Tableau Prover for Linear Logic.
10:00 - 10:30am:	Philippe de Groote, The Non-associative Lambek Calculus with Product in Polynomial Time.
10:30 - 11:00am:	Break
Session XII	Chair: (TBA)
11:00 - 11:30am:	Heribert Schütz, Generating Minimal Herbrand Models Step by Step.
11:30 - 11:50am:	Noriko H. Arai, Shinji Inoue, and Ryuji Masukawa, Sequent Decomposition: a sequent calculus as efficient as resolution.
11:50am - 12:10pm:	Miyuki Koshimura and Ryuzo Hasegawa, A Proof of Completeness for Non-Horn Magic Sets and Its Application to Proof Condensation.
12:10 - 12:30pm:	Karsten Konrad, Model Generation for Natural-Language Semantic Analysis.
12:00 - 1:30pm:	LUNCH

Back to TABLEAUX'99