12. CADE 1994: Nancy, France

Invited Talk

• John K. Slaney:
  The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure. 1-13
  

Heuristics for Induction

• Toby Walsh:
  A Divergence Critic. 14-28
  
• Dieter Hutter:
  Synthesis of Induction Orderings for Existence Proofs. 29-41
  
• Martin Protzen:
  Lazy Generation of Induction Hypotheses. 42-56
  

Experiments with Resolution Systems

• David A. Plaisted:
  The Search Efficiency of Theorem Proving Strategies. 57-71
  
• Christophe Bourely, Ricardo Caferra, Nicolas Peltier:
  A Method for Building Models Automatically. Experiments with an Extension of OTTER. 72-86
  
• Peter Baumgartner, Ulrich Furbach:
  Model Elimination Without Contrapositives. 87-101
  

Implicit vs. Explicit Induction

• François Bronsard, Uday S. Reddy, Robert W. Hasker:
  Induction using Term Orderings. 102-117
  
• Jacques Chazarain, Emmanuel Kounalis:
  Mechanizable Inductive Proofs for a Class of Forall Exists Formulas. 118-132
  
• Olav Lysne:
  On the Connection between Narrowing and Proof by Consistency. 133-147
  

Induction

• Lawrence C. Paulson:
  A Fixedpoint Approach to Implementing (Co)Inductive Definitions. 148-161
  
• Claus-Peter Wirth, Bernhard Gramlich:
  On Notions of Inductive Validity for First-Oder Equational Clauses. 162-176
  
• Siani Baker:
  A New Application for Explanation-Based Generalisation within Automated Deduction. 177-191
  

Heuristics for Controlling Resolution

• Heng Chu, David A. Plaisted:
  Semantically Guided First-Order Theorem Proving using Hyper-Linking. 192-206
  
• D. Andre de Waal, John P. Gallagher:
  The Applicability of Logic Program Analysis and Transformation to Theorem Proving. 207-221
  
• Stefan Brüning:
  Detecting Non-Provable Goals. 222-236
  

Panel Discussion

• Robert S. Boyer:
  Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We? 237
  
• The QED Manifesto. 238-251

ATP Problems

• Geoff Sutcliffe, Christian B. Suttner, Theodor Yemenis:
  The TPTP Problem Library. 252-266
  

Unification

• Eric Domenjoud, Francis Klay, Christophe Ringeissen:
  Combination Techniques for Non-Disjoint Equational Theories. 267-281
  
• Gernot Salzer:
  Primal Grammars and Unification Modulo a Binary Clause. 282-295
  

Logic Programming Applications

• Koji Iwanuma:
  Conservative Query Normalization on Parallel Circumscription. 296-310
  
• Laurent Fribourg, Marcos Veloso Peixoto:
  Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints. 311-325
  
• Véronique Royer, Joachim Quantz:
  On Intuitionistic Query Answering in Description Bases. 326-340
  

Applications

• Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood:
  Deductive Composition of Astronomical Software from Subroutine Libraries. 341-355
  
• William M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer:
  Proof Script Pragmatics in IMPS. 356-370
  
• Manfred Kerber, Michael Kohlhase:
  A Mechanization of Strong Kleene Logic for Partial Functions. 371-385
  

Special-Purpose Provers

• Dongming Wang:
  Algebraic Factoring and Geometry Proving. 386-400
  
• Nicholas Freitag McPhee, Shang-Ching Chou, Xiao-Shan Gao:
  Mechanically Proving Geometry Theorems Using a Combination of Wu's Method and Collins' Method. 401-415
  
• Larry M. Hines:
  Str+ve and Integers. 416-430
  

Banquet Speech

• Richard Platek:
  What is a Proof? (Abstract). 431
  

Invited Talk

• Ursula Martin:
  Termination, Geometry and Invariants. 432-434
  

Rewrite Rule Termination

• Leo Bachmair, Harald Ganzinger:
  Ordered Chaining for Total Orderings. 435-450
  
• Aart Middeldorp, Hans Zantema:
  Simple Termination Revisited. 451-465
  
• David A. Basin, Toby Walsh:
  Termination Orderings for Rippling. 466-483
  

ATP Efficiency

• David B. Sturgill, Alberto Maria Segre:
  A Novel Asynchronous Parallelism Scheme for First-Order Logic. 484-498
  
• Jean Goubault:
  Proving with BDDs and Control of Information. 499-513
  
• Peter Graf:
  Extended Path-Indexing. 514-528
  

Invited Talk

• Robert L. Constable:
  Exporting and Refecting Abstract Metamathematics. 529
  

AC Unification

• Laurent Vigneron:
  Associative-Commutative Deduction with Constraints. 530-544
  
• Robert Nieuwenhuis, Albert Rubio:
  AC-Superposition with Constraints: No AC-Unifiers Needed. 545-559
  
• Miki Hermann, Phokion G. Kolaitis:
  The Complexity of Counting Problems in Equational Matching. 560-574
  

Higher-Order Theorem Proving

• Penny Anderson:
  Representing Proof Transformations for Program Optimizations. 575-589
  
• Paul Jackson:
  Exploring Abstract Algebra in Constructive Type Theory. 590-604
  
• Amy P. Felty, Douglas J. Howe:
  Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables. 605-619
  

Higher-Order Unification

• Patricia Johann, Michael Kohlhase:
  Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading. 620-634
  
• Christian Prehofer:
  Decidable Higher-Order Unification Problems. 635-649
  
• Olaf Müller, Franz Weber:
  Theory and Practice of Minimal Modular Higher-Order E-Unification. 650-664
  

General Unification

• Rolf Socher-Ambrosius:
  A Refined Version of General E-Unification. 665-677
  
• Bernhard Beckert:
  A Completion-Based Method for Mixed Universal and Rigid E-Unification. 678-692
  
• Reinhard Bündgen:
  On Pot, Pans and Pudding or How to Discover Generalised Critical Pairs. 693-707
  

Natural Systems

• Stefan Klingenbeck, Reiner Hähnle:
  Semantic Tableaux with Ordering Restrictions. 708-722
  
• Fabio Massacci:
  Strongly Analytic Tableaux for Normal Modal Logics. 723-737
  
• Xiaorong Huang:
  Reconstruction Proofs at the Assertion Level. 738-752
  

Problem Sets

• Jian Zhang:
  Problems on the Generation of Finite Models. 753-757
  
• Edmund M. Clarke, Xudong Zhao:
  Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. 758-763
  

System Descriptions

• John K. Slaney, Ewing L. Lusk, William McCune:
  SCOTT: Semantically Constrained Otter System Description. 764-768
  
• Peter Baumgartner, Ulrich Furbach:
  PROTEIN: A PROver with a Theory Extension INterface. 769-773
  
• Johann Schumann:
  DELTA - A Bottom-up Preprocessor for Top-Down Theorem Provers - System Abstract. 774-777
  
• Christoph Goller, Reinhold Letz, Klaus Mayr, Johann Schumann:
  SETHEO V3.2: Recent Developments - System Abstract. 778-782
  
• Wolfgang Bibel, Stefan Brüning, Uwe Egly, Thomas Rath:
  KoMeT. 783-787
  
• Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann:
  Omega-MKRP: A Proof Development Environment. 788-792
  
• Bernhard Beckert, Joachim Posegga:
  leanT^AP: Lean Tableau-Based Theorem Proving (Extended Abstract). 793-797
  
• John K. Slaney:
  FINDER: Finite Domain Enumerator - System Description. 798-801
  
• Frederic D. Portoraro:
  Symlog: Automated Advice in Fitch-style Proof Construction. 802-806
  
• Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann:
  KEIM: A Toolkit for Automated Deduction. 807-810
  
• Frank Pfenning:
  Elf: A Meta-Language for Deductive Systems (System Descrition). 811-815
  
• Takeshi Ohtani, Hajime Sawamura, Toshiro Minami:
  EUODHILOS-II on Top of GNU Epoch. 816-820
  
• Lars-Henrik Eriksson:
  Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions. 821-825
  
• Bradley L. Richards, Ina Kraan, Alan Smaill, Geraint A. Wiggins:
  Mollusc: A General Proof-Development Shell for Sequent-Based Logics. 826-830
  
• Tie-Cheng Wang, Allen Goldberg:
  KITP-93: An Automated Inference System for Program Analysis. 831-835
  
• Adel Bouhoula:
  SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs. 836-840
  
• Maria Paola Bonacina, William McCune:
  Distributed Theorem Proving by Peers. 841-845