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

@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
  
• Melvin Fitting:
  Higher-Order Modal Logic - A Sketch. 23-38
  
• Deepak Kapur, G. Sivakumar:
  Proving Associative-Communicative Termination Using RPO-Compatible Orderings. 39-61
  
• Alexander Leitsch:
  Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction. 62-79
  
• David A. Plaisted, Yunshan Zhu:
  Replacement Rules with Definition Detection. 80-94
  

Contributed Papers

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