FTP'98International Workshop on

Technical Report E1852GS981, Technische Universität Wien, Karlsplatz 13/E1852, A1040 Wien
This page gives access to the extended abstracts presented at FTP'98 (BiBTeX entries). Full versions of most papers were published in the volume Automated Deduction in Classical and NonClassical Logics, LNCS 1761, Springer 2000.
The front matter consists of cover page, preface, list of persons involved (program committee, additional referees, steering committee), and table of contents.
Automated theorem proving
in firstorder logic modulo:
on the difference between type theory and set theory
Gilles Dowek, pages 121
(Abstract; the full version will
appear in spring 1999 in a volume on firstorder theorem proving.)
Higherorder modal logic  a sketch
Melvin Fitting, pages 2236
(Abstract; the full version will
appear in spring 1999 in a volume on firstorder theorem proving.)
Bertrand Russell, Herbrand's theorem, and the assignment statement
Melvin Fitting, pages 3749
Published in J.Calmet and J.Plaza, editors, Artificial Intelligence and
Symbolic Computation, LNCS 1476 (LNAI), Springer Verlag, 1998.
Decision procedures and model building,
or How to improve logical information in ATP
Alexander Leitsch, pages 5064
(Abstract; the full version will
appear in spring 1999 in a volume on firstorder theorem proving.)
All regular submissions were refereed by two or three referees. The program committee accepted 19 out of 24 abstracts.
Constraint contextual rewriting
Alessandro Armando and Silvio Ranise, pages 6575
How complex is a finite firstorder sorted interpretation?
Thierry Boy de la Tour, pages 7685
A further and effective liberalization of the deltarule in free variable semantic tableaux
Domenico Cantone and Marianna Nicolosi Asmundo, pages 8696
A new fast tableaubased decision procedure for an unquantified fragment of set theory
Domenico Cantone and Calogero G. Zarba, pages 97105
A partial instantiation based first order theorem prover
Vijay Chandru, John Hooker, Gabriela Rago, and Anjul Shrivastava, pages 106115
Interpretation of a Mizarlike logic in firstorder logic
Ingo Dahn, pages 116126
An O((n.log n)^3)time transformation from Grz into decidable fragments of classical firstorder logic
Stephane Demri and Rajeev Gore, pages 127134
Implicational completeness of signed resolution
Christian Fermüller, pages 135141
An equational reengineering of set theories
Andrea Formisano and Eugenio Omodeo, pages 142151
Issues of decidability for description logics in the framework of resolution
Ullrich Hustadt and Renate A. Schmidt, pages 152161
Upper bound on the height of terms in proofs with cuts
Boris Konev, pages 162171
Proof generalization and function introduction
Nicolas Peltier, pages 172181
Extending decidable clause classes via constraints
Reinhard Pichler, pages 182192
Completeness and redundancy in constrained clause logic
Reinhard Pichler, pages 193203
Effective properties for some first order intuitionistic modal logics
Aida Pliuskeviciene, pages 204212
Hidden congruent deduction
Grigore Rosu and Joseph Goguen, pages 213223
Resolutionbased theorem proving for SHnlogics
Viorica SofronieStokkermans, pages 224233
A new resolution calculus for the infinitevalued propositional logic of Lukasiewicz
Hubert Wagner, pages 234243
Full firstorder sequent and tableau calculi with preservation of solutions and the liberalized deltarule but without skolemization
ClausPeter Wirth, pages 244255
Theorem proving strategies: a search oriented taxonomy
Maria Paola Bonacina, pages 256259
Computational representations of models of firstorder formulas
Robert Matzinger, pages 260261
Verifying textbook proofs
Claus Zinn, pages 262264
The Call for Papers is available as plain text, as LaTeX source, and in PDF format.
The Final Program is available as plain text, as LaTeX source, and in PDF format.
The List of Participants is available as LaTeX source, and in PDF format.
23 Dec 1998, Gernot Salzer (ps to pdf conversion of documents 4 Jan 2018)