2. FTP 1998: Schloss Wilhelminenberg, Vienna, Austria - LNCS Volume

Ricardo Caferra, Gernot Salzer (Eds.): Automated Deduction in Classical and Non-Classical Logics, Selected Papers. Lecture Notes in Computer Science 1761 Springer 2000, ISBN 3-540-67190-0 BibTeX

@proceedings{DBLP:conf/ftp/1998,
  editor    = {Ricardo Caferra and
               Gernot Salzer},
  title     = {Automated Deduction in Classical and Non-Classical Logics, Selected
               Papers},
  booktitle = {FTP (LNCS Selection)},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1761},
  year      = {2000},
  isbn      = {3-540-67190-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Papers

Gilles Dowek:
Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory. 1-22
Electronic Edition (Springer LINK) BibTeX
Melvin Fitting:
Higher-Order Modal Logic - A Sketch. 23-38
Electronic Edition (Springer LINK) BibTeX
Deepak Kapur, G. Sivakumar:
Proving Associative-Communicative Termination Using RPO-Compatible Orderings. 39-61
Electronic Edition (Springer LINK) BibTeX
Alexander Leitsch:
Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction. 62-79
Electronic Edition (Springer LINK) BibTeX
David A. Plaisted, Yunshan Zhu:
Replacement Rules with Definition Detection. 80-94
Electronic Edition (Springer LINK) BibTeX

Contributed Papers

Thierry Boy de la Tour:
On the Complexity of Finite Sorted Algebras. 95-108
Electronic Edition (Springer LINK) BibTeX
Domenico Cantone, Marianna Nicolosi Asmundo:
A Further and Effective Liberalization of the delta-Rule in Free Variable Semantic Tableaux. 109-125
Electronic Edition (Springer LINK) BibTeX
Domenico Cantone, Calogero G. Zarba:
A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set Theory. 126-136
Electronic Edition (Springer LINK) BibTeX
Ingo Dahn:
Interpretation of a Mizar-Like Logic in First-Order Logic. 137-151
Electronic Edition (Springer LINK) BibTeX
Stéphane Demri, Rajeev Goré:
An O ((n·log n)³)-Time Transformation from Grz into Decidable Fragments of Classical First-Order Logic. 152-166
Electronic Edition (Springer LINK) BibTeX
Christian G. Fermüller:
Implicational Completeness of Signed Resolution. 167-174
Electronic Edition (Springer LINK) BibTeX
Andrea Formisano, Eugenio G. Omodeo:
An Equational Re-engineering of Set Theories. 175-190
Electronic Edition (Springer LINK) BibTeX
Ullrich Hustadt, Renate A. Schmidt:
Issues of Decidability for Description Logics in the Framework of Resolution. 191-205
Electronic Edition (Springer LINK) BibTeX
Reinhard Pichler:
Extending Decidable Clause Classes via Constraints. 206-220
Electronic Edition (Springer LINK) BibTeX
Reinhard Pichler:
Completeness and Redundancy in Constrained Clause Logic. 221-235
Electronic Edition (Springer LINK) BibTeX
Aida Pliuskeviciene:
Effective Properties of Some First-Order Intuitionistic Modal Logics. 236-250
Electronic Edition (Springer LINK) BibTeX
Grigore Rosu, Joseph A. Goguen:
Hidden Congruent Deduction. 251-266
Electronic Edition (Springer LINK) BibTeX
Viorica Sofronie-Stokkermans:
Resolution-Based Theorem Proving for SH_n-Logics. 267-281
Electronic Edition (Springer LINK) BibTeX
Claus-Peter Wirth:
Full First-Order Sequent and Tableau Calculi with Preservation of Solutions and the Liberalized delta-Rule but without Skolemization. 282-297
Electronic Edition (Springer LINK) BibTeX