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