FTP'98 - Final Program
          Schloss Wilhelminenberg, Vienna, November 23-25, 1998


Monday 23 November 1998
=======================

 9:00 Opening Address

Session I: Invited talk
-----------------------
 9:10 Decision procedures and model building, or How to improve logical
      information in ATP
      (Alexander Leitsch)

10:10 Coffee break

Session II: Constrained clause logic
------------------------------------
10:40 Proof generalization and function introduction
      (Nicolas Peltier)
11:10 Completeness and redundancy in constrained clause logic
      (Reinhard Pichler)
11:40 Extending decidable clause classes via constraints
      (Reinhard Pichler)

12:10 Lunch break

Session III: Decision procedures
--------------------------------
14:10 An O((n.log n)^3)-time transformation from Grz into decidable
      fragments of classical first-order logic
      (Stephane Demri and Rajeev Gore)
14:40 Issues of decidability for description logics in the framework
      of resolution
      (Ullrich Hustadt and Renate A. Schmidt)
15:10 A new fast tableau-based decision procedure for an unquantified
      fragment of set theory
      (Domenico Cantone and Calogero G. Zarba)

15:40 Coffee break

Session IV: Interpretation & Verification
-----------------------------------------
16:10 How complex is a finite first-order sorted interpretation?
      (Thierry Boy de la Tour)
16:40 Computational representations of models of first-order formulas
      (Robert Matzinger)
16:55 Interpretation of a Mizar-like logic in first-order logic
      (Ingo Dahn)
17:25 Verifying textbook proofs
      (Claus Zinn)



Tuesday 24 November 1998
========================

Session V: Invited talk
-----------------------
 9:00 Quantified modal logic
      (Melvin Fitting)

10:30 Coffee break

Session VI: Many-valued logics
------------------------------
11:00 Implicational completeness of signed resolution
      (Christian Fermueller)
11:30 Resolution-based theorem proving for SHn-logics
      (Viorica Sofronie-Stokkermans)
12:00 A new resolution calculus for the infinite-valued propositional
      logic of Lukasiewicz
      (Hubert Wagner)

12:30 Lunch break

Session VII: Tableaux & First-order theorem proving
---------------------------------------------------
14:30 A further and effective liberalization of the delta-rule in free
      variable semantic tableaux
      (Domenico Cantone and Marianna Nicolosi Asmundo)
15:00 Full first-order sequent and tableau calculi with preservation of
      solutions and the liberalized delta-rule but without skolemization
      (Claus-Peter Wirth)
15:30 A partial instantiation based first-order theorem prover
      (J.N. Hooker, G. Rago, Vijay Chandru, and Anjul Shrivastava)
16:00 Theorem proving strategies: a search oriented taxonomy
      (Maria Paola Bonacina)

16:15 Coffee break

Session VIII: Panel discussion
------------------------------

16:45 Concepts, logics, and research methodologies in automated deduction
      Chairs:    Maria Paola Bonacina and Ricardo Caferra
      Panelists: Domenico Cantone, Gilles Dowek, Melvin Fitting, and
                 Alexander Leitsch
        
17:45 Business meeting

19:00 Dinner at a Viennese "Heuriger"



Wednesday 25 November 1998
==========================

Session IX: Invited talk
------------------------
 9:00 Automated theorem proving in first-order logic modulo:
      on the difference between type theory and set theory
      (Gilles Dowek)

10:30 Coffee break

Session X: Equational reasoning
-------------------------------
11:00 Constraint contextual rewriting
      (Alessandro Armando and Silvio Ranise)
11:30 An equational re-engineering of set theories
      (Andrea Formisano and Eugenio Omodeo)
12:00 Hidden congruent deduction
      (Grigore Rosu and Joseph Goguen)

12:30 Lunch break

Session X: Proof theory
-----------------------
14:30 Upper bound on the height of terms in proofs with cuts
      (Boris Konev)
15:00 Effective properties for some first order intuitionistic
      modal logics
      (Aida Pliuskeviciene)

15:30 Coffee break

16:00 Closing discussion