10. CADE 1990: Kaiserslautern, Germany

Session 1: Keynote Address

• Robert S. Boyer, J. Strother Moore:
  A Theorem Prover for a Computational Logic. 1-15
  

Session 2

• Xumin Nie, David A. Plaisted:
  A Complete Semantic Back Chaining Proof System. 16-27
  
• John K. Slaney, Ewing L. Lusk:
  Parallelizing the Closure Computation in Automated Deduction. 28-39
  
• Johann Schumann, Reinhold Letz:
  PARTHEO: A High-Performance Parallel Theorem Prover. 40-56
  

Session 3

• Sang Ho Lee, Lawrence J. Henschen:
  Substitution-based Compilation of Extended Rules in Deductive Databases. 57-71
  
• Newton C. A. da Costa, Lawrence J. Henschen, James J. Lu, V. S. Subrahmanian:
  Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation. 72-86
  
• Toshiro Wakayama, T. H. Payne:
  Case-Free Programs: An Abstraction of Definite Horn Programs. 87-101
  
• Chitta Baral, Jorge Lobo, Jack Minker:
  Generalized Well-founded Semantics for Logic Programs (Extended Abstract). 102-116
  

Session 4

• Maritta Heisel, Wolfgang Reif, Werner Stephan:
  Tactical Theorem Proving in Program Verification. 117-131
  
• Alan Bundy, Frank van Harmelen, Alan Smaill, Andrew Ireland:
  Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs. 132-146
  
• Dieter Hutter:
  Guiding Induction Proofs. 147-161
  
• Uday S. Reddy:
  Term Rewriting Induction. 162-177
  

Session 5

• Hans-Jürgen Bürckert:
  A Resolution Principle for Clauses with Constraints. 178-192
  
• Larry M. Hines:
  Str+ve-Subset: The Str+ve-based Subset Prover. 193-206
  
• Shang-Ching Chou, Xiao-Shan Gao:
  Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving. 207-220
  

Session 6

• Amy P. Felty, Dale Miller:
  Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. 221-235
  
• David J. Pym, Lincoln A. Wallen:
  Investigations into Proof-Search in a System of First-Order Dependent Function Types. 236-250
  
• David A. Basin:
  Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete. 251-260
  

Session 7

• Daniel J. Dougherty, Patricia Johann:
  An Improved General E-Unification Method. 261-275
  
• Paliath Narendran, Friedrich Otto:
  Some Results on Equational Unification. 276-291
  
• Alexandre Boudet:
  Unification in a Combination of Equational Theories: an Efficient Algorithm. 292-307
  

Session 8

• Alan F. McMichael:
  SLIM: An Automated Reasoner For Equivalences, Applied To Set Theory. 308-321
  
• Mark Tarver:
  An Examination of the Prolog Technology Theorem-Prover. 322-335
  
• Frank Pfenning, Dan Nesmith:
  Presenting Intuitive Deductions via Symmetric Simplification. 336-350
  
• William Pierce:
  Toward Mechanical Methods for Streamlining Proofs. 351-365
  

Session 9

• Ursula Martin, Tobias Nipkow:
  Ordered Rewriting and Confluence. 366-380
  
• Gerald E. Peterson:
  Complete Sets of Reductions with Constraints. 381-395
  
• Franz Baader:
  Rewrite Systems for Varieties of Semigroups. 396-410
  
• Joachim Steinbach:
  Improving Assoviative Path Orderings. 411-425
  

Session 10: Invited Talk

• Wolfgang Bibel:
  Perspectives on Automated Deduction (Abstract). 426
  

Session 11

• Leo Bachmair, Harald Ganzinger:
  On Restrictions of Ordered Paramodulation with Simplification. 427-441
  
• Dan Benanav:
  Simultaneous Paramodulation. 442-455
  
• Yusuf Ozturk, Lawrence J. Henschen:
  Hyper Resolution and Equality Axioms without Function Substitutions. 456-469
  

Session 12

• Christian B. Suttner, Wolfgang Ertel:
  Automatic Acquisition of Search Guiding Heuristics. 470-484
  
• Larry Wos, S. Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler:
  Automated Reasoning Contributed to Mathematics and Logic. 485-499
  
• James A. Altucher, Prakash Panangaden:
  A Mechanically Assisted Constructive Proof in Category Theory. 500-513
  

Session 13

• Heikki Tuominen:
  Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic. 514-527
  
• Camilla Schwind:
  A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic. 528-542
  
• Peter Jackson, John Pais:
  Computing Prime Implicants. 543-557
  
• Thierry Boy de la Tour:
  Minimizing the Number of Clauses by Renaming. 558-572
  

Session 14

• Wayne Snyder:
  Higher Order E-Unification. 573-587
  
• Masami Hagiya:
  Programming by Example and Proving by Example Using Higher-order Unification. 588-602
  
• Mikael Rittri:
  Retrieving Library Identifiers via Equational Matching of Types. 603-617
  
• Werner Nutt:
  Unification in Monoidal Theories. 618-632
  

Session 15: Invited Talk

• Alan Bundy:
  A Science of Reasoning: Extended Abstract. 633-640
  

System Abstracts

• Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning:
  The TPS Theorem Proving System. 641-642
  
• Frank M. Brown, Carlos Araya:
  Schemata. 643-644
  
• Frank M. Brown, Carlos Araya:
  Cylindric Algebra Equation Solver. 645-646
  
• Alan Bundy, Frank van Harmelen, Christian Horn, Alan Smaill:
  The Oyster-Clam System. 647-648
  
• Ralph Butler, Ian T. Foster, Anita Jindal, Ross A. Overbeek:
  A High-Performance Parallel Theorem Prover. 649-650
  
• Carl Eichenlaub, Bruce Esrig, James Hook, Carl Klapper, Garrel Pottinger:
  The Romulus Proof Checker. 651-652
  
• William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
  IMPS: An Interactive Mathematical Proof System. 653-654
  
• Bernhard Gramlich:
  UNICOM: A Refined Completion Based Inductive Theorem Prover. 655-656
  
• Thomas Käufl, Nicolas Zabel:
  The Theorem Prover of the Program Verifier Tatzelwurm. 657-658
  
• Matt Kaufmann:
  RCL: A Lisp Verification System. 659-660
  
• Pierre Lescanne:
  ORME: An Implementation of Completion Procedures as Sets of Transition Rules. 661-662
  
• William McCune:
  OTTER 2.0. 663-664
  
• Neil V. Murray, Erik Rosenthal:
  DISSOLVER: A Dissolution-based Theorem Prover. 665-666
  
• Robert Nieuwenhuis, Fernando Orejas, Albert Rubio:
  TRIP: An Implementation of Clausal Rewriting. 667-668
  
• John L. Pollock:
  OSCAR. 669-670
  
• Ronald W. Satz:
  EXPERT THINKER: An Adaptation of F-Prolog to Microcomputers. 671-672
  
• Mark E. Stickel:
  A Prolog Technology Theorem Prover. 673-674
  
• Geoff Sutcliffe:
  A General Clause Theorem Prover. 675-676
  
• Andrei Voronkov:
  LISS - The Logic Inference Search System. 677-678
  
• David A. Wolfram:
  ACE: The Abstract Clause Engine. 679-680
  

Tutorials

• Ewing L. Lusk, William McCune:
  Tutorial on High-Performance Automated Theorem Proving. 681
  
• Jürgen Müller, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka:
  Tutorial on Reasoning and Representation with Concept Languages. 681
  
• Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning:
  Tutorial on Lambda-Prolog. 682
  
• Claude Kirchner:
  Tutorial on Equational Unification. 682
  
• Hans Jürgen Ohlbach, Andreas Herzig:
  Tutorial on Compilation techniques for Logics. 683
  
• Johann Schumann, Reinhold Letz, Franz J. Kurfess:
  Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation. 683
  
• Jieh Hsiang, Jean-Pierre Jouannaud:
  Tutorial on Rewrite-Based Theorem Proving. 684
  
• Richard J. Waldinger:
  Tutorial on Program-Synthetic Deduction. 684
  
• Paul Pritchard, John K. Slaney:
  Tutorial on Computing Models of Propositional Logics. 685