10. CADE 1990: Kaiserslautern, Germany
Mark E. Stickel (Ed.): 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings. Springer 1990 Lecture Notes in Computer Science ISBN 3-540-52885-7
Session 1: Keynote Address
Session 2
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
- 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
- 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
- William Pierce: Toward Mechanical Methods for Streamlining Proofs. 351-365
Session 9
- 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
- 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
- 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
- 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
- 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
- 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
- Jürgen Müller, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka: Tutorial on Reasoning and Representation with Concept Languages. 681
- Claude Kirchner: Tutorial on Equational Unification. 682
- Johann Schumann, Reinhold Letz, Franz J. Kurfess: Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation. 683
- Richard J. Waldinger: Tutorial on Program-Synthetic Deduction. 684
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T203413 by the dblp team