------------------------------------------------------------------------- FTP 2000 and TABLEAUX 2000 Call for Participation University of St Andrews St Andrews, Scotland July 3-7, 2000 FTP 2000: http://www.uni-koblenz.de/ftp00/ TABLEAUX 2000: http://www-theory.dcs.st-and.ac.uk/~rd/tab2000/ --------------------------------------------------------------------- Contents: 1 - Scope 2 - Registration 3 - Contact 4 - Technical Program (including list of accepted contributions) --------------------------------------------------------------------- 1 - Scope FTP 2000 (First-Order Theorem Proving), July 3-5, is the third in a series of workshops intended to focus effort on First-Order Theorem Proving as a core theme of Automated Deduction, and to provide a forum for presentation of very recent work and discussion of research in progress. TABLEAUX 2000, July 4-7, is a continuation of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods held since 1992. 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. FTP 2000 is held in conjunction with TABLEAUX 2000. The FTP 2000 and TABLEAUX 2000 sessions will be partly in series, partly shared and partly in parallel. --------------------------------------------------------------------- 2 - Registration To register for FTP 2000 and/or TABLEAUX 2000 please use the online registration form at http://www.dcs.st-and.ac.uk/~tab2000/register.html Joint registration at reduced rate is possible. Early registration ends at May, 31. --------------------------------------------------------------------- 3 - Contact FTP 2000 related: ftp00@cs.uiowa.edu TABLEAUX 2000 related: rd@dcs.st-and.ac.uk Local Organisation: rd@dcs.st-and.ac.uk --------------------------------------------------------------------- 4 - Technical Program FTP 2000 and TABLEAUX 2000 schedule: http://www.dcs.st-and.ac.uk/~tab2000/schedule.html Invited Talks ------------- FTP 2000 TABLEAUX 2000 -------- ------------- David Crocker Melvin Fitting (CUNY) (Intelligent Micro Modality and Databases Software Ltd) First Order Theorem Proving in Software Verification Deepak Kapur (New Mexico) Alasdair Urquhart (Toronto) 'Hardware Verification' Local Symmetries in (exact title to be announced) Propositional Logic Franz Baader (Aachen) (Joint invited speaker) Tableau Algorithms for Description Logics FTP 2000 accepted contributions: -------------------------------- J. Avenhaus, T. Hillenbrand, B. Loechner On Using Ground Joinable Equations in Equational Theorem Proving Johan Belinfante The Unifying Concept of Subvariance Domenico Cantone The decision problem in graph theory with reachability related constructs Michael Dierkes Defining a Unique Herbrand Model for Sets of Guarded Clauses Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt Hyperresolution for Guarded Formulae Martin Giese A First-Order Simplification Rule with Constraints Koji Iwanuma, Katsumi Inoue, Ken Satoh Completeness of Pruning Methods for Consequence Finding Procedure SOL James J. Lu, Jeffrey S. Rosenthal, Andrew Shaffer Crossword Puzzles: A Case Study in Compute-Intensive Meta-Reasoning Nicolas Peltier Combining Resolution and Enumeration for Finite Model Building Reinhard Pichler Equational Problems over a Finite Domain Regimantas Pliuskevicius On \omega­decidability for a restricted FTL with Unless J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo, F. Martin A mechanical proof of Knuth-Bendix critical pair theorem (using ACL2) Nicolas Peltier Model Building with Ordered Resolution Cesare Tinelli Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing Bernhard Gramlich Extending First-Order Unification by Tractable Second-Order Features Kahlil Hodgson, John Slaney Semantic Guidance for Saturation­Based Theorem Proving Bernhard Beckert Depth­first Proof Search without Backtracking for Free Variable Clausal Tableaux Jens Otten, Wolfgang Bibel leanCoP: Lean Connection­Based Theorem Proving (system description) Position Papers Chris Fermueller Automated Model Building for Non-Classical Logics Martin Giese Proof Search without Backtracking using Instance Streams Markus Moschner Towards Finite Model Building for Propositional Gödel-Logics TABLEAUX 2000 accepted contributions ------------------------------------ Comparison of Theorem Provers for non-classical logics: Fabio Massacci and Francesco M. Donini Design and results of TANCS-2000 non-classical (modal) systems comparison Volker Haarslev and Ralf Möller Consistency testing: the RACE experience Ian Horrocks Benchmark analysis with FaCT Ullrich Hustadt and Renate Schmidt MSPASS Modal reasoning by translation and first-order resolution Peter F. Patel-Schneider TANCS-2000 results for DLP Armando Tacchella Evaluating *SAT on TANCS 2000 benchmarks Research Papers: Alberto Artosi, Guido Governatori and Antonino Rotolo A labelled tableau calculus for nonmonotonic (cumulative) consequence relations Arnon Avron A tableau system for Gödel-Dummett logic based on a hypersequent calculus Matthias Baaz, Christian Fermüller and Helmut Veith An analytic calculus for quantified propositional Gödel logic Diderik Batens and Joke Meheus A tableau method for inconsistency-adaptive logics Domenico Cantone and Calogero G. Zarba A tableau calculus for integrating first-order reasoning with elementary set theory reasoning Agata Ciabattoni and Mauro Ferrari Hypertableau and path-hypertableau calculi for some families of intermediate logics Marta Cialdea Mayer and Serenella Cerrito Variants of first-order modal logics Stéphane Demri Complexity of simple dependent bimodal logics Uwe Egly Properties of Embeddings from Int to S4 Melvin Fitting, Lars Thalmann and Andrei Voronkov Term-modal logics Enrico Giunchiglia and Armando Tacchella A subset-matching size-bounded cache for satisfiability in modal logics Rajeev Goré Dual intuitionistic logic revisited Ray Gumb Model sets in a nonconstructive logic of partial terms with definite descriptions Ortrun Ibens Search space compression in connection tableau calculi using disjunctive constraints Christoph Kreitz and Brigitte Pientka Matrix-based inductive theorem proving Pedro J. Martín and Antonio Gavilanes Monotonic preorders for free variable tableaux Maarten Marx, Szabolcs Mikulás and Mark Reynolds The mosaic method for temporal logics Linh Anh Nguyen Sequent-like tableau systems with the analytic superformula property for the modal logics KB, KDB, K5, KD5 David Pearce, Inmaculada P. de Guzmán and Agustín Valverde A tableau calculus for equilibrium entailment Carla Piazza and Alberto Policriti Towards tableau-based decision procedures for non-well-founded fragments of set theory Riccardo Rosati Tableau calculus for only knowing and knowing at most Stephan Schmitt A tableau-like representation framework for efficient proof reconstruction Dan Willard The semantic tableaux version of the second incompleteness theorem extends almost to Robinson's arithmetic Q System Descriptions: Joachim Draeger Redundancy-free lemmatization in the automated model-elimination theorem prover AI-SETHEO Gernot Stenz and Andreas Wolf E-SETHEO: An automated3 theorem prover --------------------------------------------------------------------- -- Peter Baumgartner phone: +49 261 287 2777 mail: peter@uni-koblenz.de fax: +49 261 287 2731 WWW: http://www.uni-koblenz.de/~peter/