Subject: categories: FTP 2000 and TABLEAUX 2000 - Call for Participation

From: Peter Baumgartner <[email-masked]>
Date: Mon, 22 May 2000 14:02:10 +0200 (CEST)

-------------------------------------------------------------------------

    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:      [email-masked]
TABLEAUX 2000 related: [email-masked]
Local Organisation:    [email-masked]

---------------------------------------------------------------------
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 \omegadecidability 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 SaturationBased Theorem Proving
      
Bernhard Beckert 
    Depthfirst Proof Search without Backtracking for Free Variable
    Clausal Tableaux
      
Jens Otten, Wolfgang Bibel 
    leanCoP: Lean ConnectionBased 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: [email-masked]
fax:   +49 261  287 2731    WWW:  http://www.uni-koblenz.de/~peter/