14. CADE 1997: Townsville, North Queensland, Australia

Session 1: Invited Lecture

• Wu Wen-Tsün:
  The Char-Set Method and Its Applications to Automated Reasoning. 1-3
  

Session 2

• Irène Durand, Aart Middeldorp:
  Decidable Call by Need Computations in term Rewriting (Extended Abstract). 4-18
  
• Franz Baader, Cesare Tinelli:
  A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. 19-33
  
• Joachim Niehren, Manfred Pinkal, Peter Ruhrberg:
  On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting. 34-48
  

Session 3: System Descriptions

• Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo:
  Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. 49-52
  
• Maria Paola Bonacina:
  The Clause-Diffusion Theorem Prover Peers-mcd (System Description). 53-56
  
• Bernd I. Dahn, Jürgen Gehne, Th. Honigmann, Andreas Wolf:
  Integration of Automated and Interactive Theorem Proving in ILP. 57-60
  
• Andreas Wolf, Johann Schumann:
  ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output. 61-64
• Bernd Fischer, Johann Schumann:
  SETHEO Goes Software Engineering: Application of ATP to Software Reuse. 65-68
  
• Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel:
  Proving System Correctness with KIV 3.0. 69-72
  

Session 4

• Lu Yang, Hongguang Fu, Zhenbing Zeng:
  A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry. 73-86
  
• Johann Schumann:
  Automatic Verification of Cryptographic Protocols with SETHEO. 87-100
  
• Nikolaj Bjørner, Mark E. Stickel, Tomás E. Uribe:
  A Practical Integration of First-Order Reasoning and Decision Procedures. 101-115
  

Session 5

• Uwe Egly:
  Some Pitfalls of LK-to-LJ Translations and How to Avoid Them. 116-130
  
• Daniel S. Korn, Christoph Kreitz:
  Deciding Intuitionistic Propositional Logic via Translation into Classical Logic. 131-145
  

Session 6

• Koji Iwanuma:
  Lemma Matching for a PTTP-based Top-down Theorem Prover. 146-160
  
• Olivier Roussel, Philippe Mathieu:
  Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case. 161-175
  
• Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura:
  Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving. 176-190
  

Session 7: Invited Lecture

• Moshe Y. Vardi:
  Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. 191-206
  

Session 8

• Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt:
  Connection-Based Proof Construction in Linear Logic. 207-221
  
• James Harland, David J. Pym:
  Resource-Distribution via Boolean Constraint (Extended Abstract). 222-236
  
• Mary Cryan, Allan Ramsay:
  Constructing a Normal Form for Property Theory. 237-251
  

Session 9: System Descriptions

• Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, Volker Sorge:
  Omega: Towards a Mathematical Assistant. 252-255
  
• Thomas Kolbe, Jürgen Brauburger:
  Plagiator - A Learning Prover. 256-259
  
• Dirk Fuchs, Matthias Fuchs:
  CODE: A Powerful Prover for Problems of Condensed Detachment. 260-263
  
• Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani:
  A New Method for Testing Decision Procedures in Modal Logics. 264-267
  
• John K. Slaney:
  Minlog: A Minimal Logic Theorem Prover. 268-271
  
• Hantao Zhang:
  SATO: An Efficient Propositional Prover. 272-275
  

Session 10

• Louise A. Dennis, Alan Bundy, Ian Green:
  Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs. 276-290
  
• Dieter Hutter, Michael Kohlhase:
  A Colored Version of the Lambda-Calculus. 291-305
  
• Seán Matthews:
  A Practical Implementation of Simple Consequence Relations Using Inductive Definitions. 306-320
  

Session 11

• Harald Ganzinger, Christoph Meyer, Christoph Weidenbach:
  Soft Typing for Ordered Resolution. 321-335
  
• Hans de Nivelle:
  A Classification of Non-liftable Orders for Resolution. 336-350
  

Session 12

• Amy P. Felty, Douglas J. Howe:
  Hybrid Interactive Theorem Proving Using Nuprl and HOL. 351-365
  
• Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant:
  Proof Tactics for a Theory of State Machines in a Graphical Environment. 366-379
  
• David von Oheimb, Thomas F. Gritzner:
  RALL: Machine-Supported Proofs for Relation Algebra. 380-394
  

Session 13: System Descriptions

• Jason J. Hickey:
  Nuprl-Light: An Implementation Framework for Higher-Order Logics. 395-399
  
• Maris A. Ozols, Anthony Cant, Katherine A. Eastaughffe:
  XIsabelle: A System Description. 400-403
  
• Helen Lowe, David Duncan:
  XBarnacle: Making Theorem Provers More Accessible. 404-407
  
• Mathias Kettner, Norbert Eisinger:
  The Tableau Browser SNARKS. 408-411
  
• Richard Bornat, Bernard Sufrin:
  Jape: A Calculator for Animating Proof-on-Paper. 412-415
  

Session 14

• Matthias Fuchs:
  Evolving Combinators. 416-430
  
• Gilles Défourneaux, Nicolas Peltier:
  Partial Matching for Analogy Discovery in Proofs and Counter-Examples. 431-445
  
• Jürgen Ehrensberger, Claus Zinn:
  DiaLog: A System for Dialogue Logic. 446-460