MONDAY, JUNE 7, 1999

5:00 - 8:00pm:Registration (The Inn at Saratoga; also, 9am-5pm, Tues. & Wed.)
7:00 - 9:00pm:Reception (The Inn at Saratoga)


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.


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)


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

Last updated March 10, 1999