TABLEAUX'99 International Conference on Analytic Tableaux and Related Methods The Inn at Saratoga 231 Broadway Saratoga Springs, NY USA tel. 1-800-274-3573, fax. (518) 583-2543 http://www.theinnatsaratoga.com/reserv June 7 - 11, 1999 ____________________________________ / \ / Please point your browser to \ < http://www.cs.albany.edu/~nvm/tab99/ > \ or consult the message below. / \____________________________________/ This conference is a continuation of international meetings on Theorem Proving with Analytic Tableaux and Related Methods held in Lautenbach near Karlsruhe (1992), Marseille (1993), Abingdon near Oxford (1994), St. Goar near Koblenz (1995), Terrasini near Palermo (1996), Pont-à-Mousson near Nancy (1997), and Oisterwijk near Tilburg (1998). In June 1999, the conference will for the first time be held in North America, at Saratoga Springs, NY. Since Tableaux'95, the proceedings have been published in Springer's LNAI series and will be again for 1999. The Tableaux'99 conference will have a Comparison of theorem provers for non classical (modal) systems. This comparison is organized by Fabio Massacci of Universita di Roma "La Sapienza" (e-mail: massacci@dis.uniroma1.it). Two TUTORIALS will be part of the conference program. The proceedings will be published in the LNAI series of Springer-Verlag. INVITED SPEAKERS Randy Bryant (Carnegie Mellon Univ., USA) David S. Warren (SUNY Stony Brook, USA) TOPICS Tableau methods have been found to be a convenient formalism for automating deduction in various non-standard logics as well as in classical logic. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, and system diagnosis. The conference brings together researchers interested in all aspects -- theoretical foundations, implementation techniques, systems development and applications -- of the mechanization of reasoning with tableaux and related methods. PROGRAM COMMITTEE P. Baumgartner (Koblenz Univ, Germany) B. Beckert (U. Karlsruhe, Germany) K. Broda (Imperial College, London, UK) R. Dyckhoff (St Andrews Univ, UK) A. Felty (Bell Labs, USA) C. Fermueller (TU Wien, Austria) M. Fitting (CUNY, New York City, USA) U. Furbach (Koblenz Univ, Germany) D. Galmiche (LORIA, Nancy, France) R. Gore (Austr. National Univ, Australia) P. Hodas (Harvey Mudd College, California, USA) J. Goubault-Larrecq (GIE Dyade, France) R. Haehnle (Karlsruhe Univ, Germany) C. Kreitz (Cornell Univ., USA) R. Letz (TU Munich, Germany) D. Miller (Penn State Univ., USA) U. Moscato (Milan Univ, Italy) N. Murray (SUNY at Albany, USA) Program Chair N. Olivetti (Torino Univ, Italy) J. Pitt (Imperial College, London, UK) E. Rosenthal (Univ of New Haven, USA) P. Schmitt (Karlsruhe Univ, Germany) H. de Swart (Tilburg Univ, The Netherlands) SCIENTIFIC PROGRAM INVITED TALKS Randall Bryant, (TBA) Davis S. Warren, (TBA) TUTORIALS Fabio Massacci, Automated Reasoning and the Verification of Security Protocols. Reiner Haehnle and Bernhard Beckert, Proof Confluent Tableau Calculi. ACCEPTED PAPERS FOR TABLEAUX'99 Comparison: Fabio Massacci, Introduction and Summary. - Peter F. Patel-Schneider, Description Logic Prover (DLP). - Volker Haarslev and Ralf Moeller, HAM-ALC Description Logic Reasoner. - Vijay Boyapati and Rajeev Goré, KtSeqC: A theorem prover for the minimal tense logic Kt. Research Papers (A) and System Descriptions (B): Matthias Baaz & Christian Fermueller, Analytic Calculi for Projective Logics. (A) Peter Baumgartner, Joe Horton, and Bruce Spencer, Merge Path Improvements for Minimal Model Hyper Tableaux. (A) Krysia Broda and Dov Gabbay, A Compiled Labelled Deductive System for Propositional Intuitionistic Logic. (A) James Caldwell, Intuitionisitic Tableau Extracted. (A) Domenico Cantone and Calogero G. Zarba, A tableau-based decision procedure for a fragment of set theory involving a restricted form of quantification. (A) Agata Ciabattoni, Bounded contraction in systems with linearity. (A) Philippe de Groote, The Non-associative Lambek Calculus with Product in Polynomial Time. (A) Stephane Demri, Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization? (A) Stephane Demri and Rajeev Gore, Cut-free Display Calculi for Nominal Tense Logics. (A) Joachim Draeger and Andreas Wolf, Strategy Parallel Use of Model Elimination with Lemmata - System Abstract -. (B) Ulrich Endriss, An Interactive Theorem Proving Assistant. (B) Ulrich Endriss, A Time Efficient KE Based Theorem Prover. (B) Martin Giese and Wolfgang Ahrendt, Hilbert's Epsilon-Terms in Automated Theorem Proving. (A) Paul C. Gilmore, Partial Functions in an Impredicative Simple Theory of Types. Jean.Goubault-Larrecq, A Simple Sequent System for First-Order Logic with Free Constructors. (A) Heiko Mantel and Jens Otten, linTAP: A Tableau Prover for Linear Logic. (A) Wolfgang May, A Tableau Calculus for a Temporal Logic with Temporal Connectives. (A) Christof Monz and Maarten de Rijke, A Tableaux Calculus for Pronoun Resolution. (A) Heribert Schuetz, Generating Minimal Herbrand Models Step by Step. (A) Miroslava Tzakova, Tableau Calculi for Hybrid Logics. (A) Claus-Peter Wirth, Full First-Order Free Variable Sequents and Tableaux in Implicit Induction. (A) Position papers Noriko H. Arai and Ryuji Masukawa, Sequent Decomposition: a sequent calculus as efficient as resolution. Bernhard Beckert, Depth-first Proof Search without Backtracking for Free Variable Semantic Tableaux. Marco Benini, Ugo Moscato and Alessandro Avellone, Tactics for Translation of Tableau in Natural Deduction. Uwe Egly and Hans Tompits, Gentzen-Like Methods in Quantum Logic. Shigeki Hagihara and Naoki Yonezaki, Unification-based Proof Method for Modal Logic with Well-founded Frames. Karsten Konrad, Model Generation for Natural-Language Semantic Analysis. Miyuki Koshimura and Ryuzo Hasegawa, A Proof of Completeness for Non-Horn Magic Sets and Its Application to Proof Condensation. Karl-Michael Schneider, An Application of Labelled Tableaux to Parsing. Claus Zinn, COLOSSEUM \- An Automated Theorem Prover for Intuitionistic Predicate Logic based on Dialogue Games. P.J. Martin, A. Gavilanes, Simultaneous Sorted Unification for Free Variable Tableaux: An Elegant Calculus. Dirk Fuchs and Marc Fuchs, Goal Lift-up: A Technique for Improving Proof Search in Connection Tableau Calculi. Preliminary Program Arrival Monday, June 7, 1999; Reception 7:00 - 9:15 pm Beginning of Conference: Tuesday, June 8, 1999, 9:00 am End of Conference: Friday, June 11, 1999, 12:30 pm The program consists of: 2 invited talks; 2 tutorials; a comparison of theorem provers for non classical (modal) systems; 18 talks presenting original research papers (category A); 3 talks presenting original system descriptions (category B); 9 talks presenting position papers. CALL FOR PARTICIPATION and REGISTRATION REGISTRATION AND ACCOMMODATION Before May 1, 1999 After May 1, 1999 Registration fee $280 $310 Registration fee (student) $130 $130 Tutorial fee (regular) $30 $30 Tutorial fee (student) free free Accommodation fee: $70/night (Mon. - Th.) Extra Banquet Tickets: $38 each. The accommodation fee is a special per room rate for conference attendees (1 or 2 persons) at the Conference Hotel during the conference. Other nights are at the regular rate of $90. The registration fee includes the admission to the entire conference program, a copy of the Proceedings of the conference in the LNAI series of Springer, tea or coffee in the breaks, the welcome reception at the Inn at Saratoga, breakfast and lunch Tuesday through Friday, and the conference banquet. The tutorial fee will help cover costs of materials including duplication. CONFERENCE REGISTRATION FORM (plaintext) Registration form for TABLEAUX'99 To be returned by e-mail, fax or surface mail to the registration address: Neil V. Murray, TABLEAUX'99 Institute for Programming & Logics Department of Computer Science LI-67A University at Albany - SUNY Albany, NY 12222 USA Phone: (518) 442-3393 Fax: (518) 442-5638 e-mail: tab99@cs.albany.edu Personal information Family name: __________________________ First name: _________________ Affiliation: _________________________________________________________ Address: _____________________________________________________________ E-mail: ______________________________________________________________ Tel. no: ____________________ Fax no: _____________________ Schedule My arrival time will be: _____________________________ My departure time will be: _____________________________ Accommodation Number of persons The Inn at Saratoga ____ (Register directly with The Inn) Other Hotel ____ (I am making my own arrangements) (Point your browser to http://www.spa.net/webtest/wow.htm and select Hotels/Motels/Cottages to investigate nearby accommodations.) Special dietary requirements: None ___ Vegetarian ___ Other ___ Please fill in amounts: Before May 1 After May 1 Applicable Fee: Registration fees $280.00 $310.00 Registration fees (student) $130.00 $130.00 $___________ Tutorial Fees: (Choose 1): Applicable Fee: Tutorial 1 (Regular) $30.00 Tutorial 1 (Student) Free Tutorial 2 (Regular) $30.00 Tutorial 2 (Student) Free $___________ Extra Banquet Ticket(s)($38.00 each) Banquet Total = $___________ TOTAL PAYMENT = $________________ Payment (CREDIT CARD) Payments in US Dollars can be made as follows: Please check the appropriate choice: MasterCard (EuroCard) ___ VISA ___ Expiration (Mo./Yr.) ________________ Cardnumber _________________________________________________________ Payment (CASH) Check in dollars drawn on a US bank; made payable to University at Albany. Please put TABLEAUX'99 on the memo line. IMPORTANT NOTE: all extra fees emerging from check or money order payment must be covered by the applicant. If you are paying by credit card, you must FAX or MAIL hard copy of this form with your signature. If you also email this form, DO NOT include credit card information - that should be on the hard copy only. Date: __________________________ Signature: __________________________________________ Conference site SARATOGA SPRINGS, NY USA Home of the oldest thoroughbred race track in the US, Saratoga Springs is a delightful village about 290 km north of New York City. For over 130 years, many legendary horses have run here: Man O'War won five times, but also suffered his only loss. Triple Crown winner Secretariat was also upset here, at the track often called the ``graveyard of favorites''. Across from the track is the National Museum of Racing and Hall of Fame. Saratoga's attractions, however, go far beyond racing. On the site of the Saratoga Nationial Historic Park, the British forces surrendered to the Colonials on October 17, 1777 - an event considered the turning point of the American Revolution. Nineteenth century architecture is still present in Saratoga, from Gothic gables and stained glass windows to charming gazebos and gingerbread porches. Over 1000 buildings are on the National Register of Historic Places. The beautiful Yaddo Gardens were opened in 1881; since 1922, the mansion has been preserved as a peaceful and private sanctuary for writers, poets, painters and composers. In the heart of the Saratoga Spa State Park are the Roosevelt Mineral Baths, where you may indulge yourself submerging in a deep, soothing tub of naturally carbonated spring water. The National Museum of Dance is the only museum in the US devoted exclusively to professional American dance - from ballet to Broadway, modern to jazz, ethnic to tap. Opened in 1986, the museum offers exhibits, master classes, educational programs, and conversations with visiting dancers. It is one program of the Saratoga Performing Arts Center (SPAC). An open air theater, SPAC hosts classical presentations by the New York City Ballet, New York City Opera, and Philadelphia Orchestra. It is also the venue of about 30 contemporary events including the Newport Jazz festival and many popular bands. Saratoga also boasts lovely downtown shopping districts with elegant boutiques. There, and in the surrounding countryside, many antique shops can be found. Sidewalk cafes, lakeside restaurants, Country Inns, and award winning restaurants and bistros suit both the gourmet and casual diner. MORE INFORMATION E-mail: nvm@cs.albany.edu WWW: http://www.cs.albany.edu/~nvm/tab99/