|
|
FTP'98International Workshop on
|
Technical Report E1852-GS-981, Technische Universität Wien, Karlsplatz 13/E1852, A-1040 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 Non-Classical 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 first-order logic modulo:
on the difference between type theory and set theory
Gilles Dowek, pages 1-21
(Abstract; the full version will
appear in spring 1999 in a volume on first-order theorem proving.)
Higher-order modal logic - a sketch
Melvin Fitting, pages 22-36
(Abstract; the full version will
appear in spring 1999 in a volume on first-order theorem proving.)
Bertrand Russell, Herbrand's theorem, and the assignment statement
Melvin Fitting, pages 37-49
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 50-64
(Abstract; the full version will
appear in spring 1999 in a volume on first-order 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 65-75
How complex is a finite first-order sorted interpretation?
Thierry Boy de la Tour, pages 76-85
A further and effective liberalization of the delta-rule in free variable semantic tableaux
Domenico Cantone and Marianna Nicolosi Asmundo, pages 86-96
A new fast tableau-based decision procedure for an unquantified fragment of set theory
Domenico Cantone and Calogero G. Zarba, pages 97-105
A partial instantiation based first order theorem prover
Vijay Chandru, John Hooker, Gabriela Rago, and Anjul Shrivastava, pages 106-115
Interpretation of a Mizar-like logic in first-order logic
Ingo Dahn, pages 116-126
An O((n.log n)^3)-time transformation from Grz into decidable fragments of classical first-order logic
Stephane Demri and Rajeev Gore, pages 127-134
Implicational completeness of signed resolution
Christian Fermüller, pages 135-141
An equational re-engineering of set theories
Andrea Formisano and Eugenio Omodeo, pages 142-151
Issues of decidability for description logics in the framework of resolution
Ullrich Hustadt and Renate A. Schmidt, pages 152-161
Upper bound on the height of terms in proofs with cuts
Boris Konev, pages 162-171
Proof generalization and function introduction
Nicolas Peltier, pages 172-181
Extending decidable clause classes via constraints
Reinhard Pichler, pages 182-192
Completeness and redundancy in constrained clause logic
Reinhard Pichler, pages 193-203
Effective properties for some first order intuitionistic modal logics
Aida Pliuskeviciene, pages 204-212
Hidden congruent deduction
Grigore Rosu and Joseph Goguen, pages 213-223
Resolution-based theorem proving for SHn-logics
Viorica Sofronie-Stokkermans, pages 224-233
A new resolution calculus for the infinite-valued propositional logic of Lukasiewicz
Hubert Wagner, pages 234-243
Full first-order sequent and tableau calculi with preservation of solutions and the liberalized delta-rule but without skolemization
Claus-Peter Wirth, pages 244-255
Theorem proving strategies: a search oriented taxonomy
Maria Paola Bonacina, pages 256-259
Computational representations of models of first-order formulas
Robert Matzinger, pages 260-261
Verifying textbook proofs
Claus Zinn, pages 262-264
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)