default search action
9th CADE 1988: Argonne, Illinois, USA
- Ewing L. Lusk, Ross A. Overbeek:
9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings. Lecture Notes in Computer Science 310, Springer 1988, ISBN 3-540-19343-X
Session 1
- Hantao Zhang, Deepak Kapur:
First-Order Theorem Proving Using Conditional Rewrite Rules. 1-20 - Tie-Cheng Wang:
Elements of Z-Module Reasoning. 21-40
Session 2
- Michael R. Donat, Lincoln A. Wallen:
Learning and Applying Generalised Solutions using Higher Order Resolution. 41-60 - Amy P. Felty, Dale Miller
:
Specifying Theorem Provers in a Higher-Order Logic Programming Language. 61-80 - V. S. Subrahmanian:
Query Processing in Quantitative Logic Programming. 81-100
Session 3
- David A. Basin:
An Environment For Automated Reasoning About Partial Functions. 101-110 - Alan Bundy:
The Use of Explicit Plans to Guide Inductive Proofs. 111-120 - D. Duchier, Drew V. McDermott:
LOGICALC: An Environment for Interactive Proof Development. 121-130
Session 4
- Maritta Heisel, Wolfgang Reif
Implementing Verification Strategies in the KIV-System. 131-140 - Donald Simon:
Checking Natural Language Proofs. 141-150 - Marc Bezem:
Consistency of Rule-based Expert System. 151-161
Session 5
- Hantao Zhang, Deepak Kapur, Mukkai S. Krishnamoorthy:
A Mechanizable Induction Principle for Equational Specifications. 162-181 - Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder:
Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time. 182-196
Session 6
- Michael A. McRobbie, Robert K. Meyer, Paul B. Thistlewaite:
Towards Efficient "Knowledge-Based" Automated Theorem Proving for Non-Standard Logics. 197-217 - A. A. Aaby, K. T. Narayana:
Propositional Temporal Interval Logic is PSPACE Complete. 218-237
Session 7
- Douglas J. Howe:
Computational Metatheory in Nuprl. 238-257 - H. Azzoune:
Type Inference in Prolog. 258-277
Session 8
- Jack Minker, Arcot Rajasekar:
Procedural Interpretation of Non-Horn Logic Programs. 278-293 - Shan Chi, Lawrence J. Henschen:
Recursive Query Answering with Non-Horn Clauses. 294-312
Session 9
- Toshiro Wakayama, T. H. Payne:
Case Inference in Resolution-Based Languages. 313-322 - Ralph Butler, Rasiah Loganantharaj, Robert Olson:
Notes on Prolog Program Transformations, Prolog Style, and Efficient Compilation to The Warren Abstract Machine. 323-332 - Ralph Butler, Nicholas T. Karonis:
Exploitation of Parallelism in Prototypical Deduction Problems. 333-343
Session 10
- Louise E. Moser:
A Decision Procedure for Unquantified Formulas of Graph Theory. 344-357 - Patrick Lincoln, Jim Christian:
Adventures in Associative-Commutative Unification (A Summary). 358-367 - Wolfram Büttner:
Unification in Finite Algebras is Unitary (?). 368-377
Session 11
- Manfred Schmidt-Schauß:
Unification in a Combination of Arbitrary Disjoint Equational Theories. 378-396 - Karl-Hans Bläsius, Jörg H. Siekmann:
Partial Unification for Graph Based Equational Reasoning. 397-414
Session 12
- Rainer Manthey, François Bry
SATCHMO: A Theorem Prover Implemented in Prolog. 415-434 - Richard C. Potter, David A. Plaisted:
Term Rewriting: Some Experimental Results. 435-453
Session 13
- Bishop Brock, Shaun Cooper, William Pierce:
Analogical Reasoning and Proof Discovery. 454-468 - Larry M. Hines:
Hyper-Chaining and Knowledge-Based Theorem Proving. 469-486
Session 14
- Luis Fariñas del Cerro, Andreas Herzig:
Linear Modal Deductions. 487-499 - Hans Jürgen Ohlbach:
A Resolution Calculus for Modal Logics. 500-516
Session 15
- Hans-Jürgen Bürckert:
Solving Disequations in Equational Theories. 517-526 - Emmanuel Kounalis, Michaël Rusinowitch:
On Word Problems in Horn Theories. 527-537 - Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar:
Canonical Conditional Rewrite Systems. 538-549 - Paul Jacquet:
Program Synthesis by Completion with Dependent Subtypes. 550-562
Session 16
- Thomas Käufl:
Reasoning about Systems of Linear Inequalities. 563-572 - Rolf Socher:
A Subsumption Algorithm Based on Characteristic Matrices. 573-581 - Arkady Rabinov:
A Restriction of Factoring in Binary Resolution. 582-591 - Philippe Besnard, Pierre Siegel:
Supposition-Based Logic for Automated Nonmontonic Reasoning. 592-601
Session 17
- Christoph Walther:
Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. 602-621 - Leo Marcus, Timothy Redmond:
Two Automated Methods in Implementation Proofs. 622-642
Session 18
- Mark Franzen, Lawrence J. Henschen:
A New Approach to Universal Unification and Its Application to AC-Unification. 643-657 - Neil V. Murray, Erik Rosenthal:
An Implementation of a Dissolution-Based System Employing Theory Links. 658-674
Session 19
- Ilkka Niemelä:
Decision Procedure for Autoepistemic Logic. 675-684 - Peter K. Malkin, Errol P. Martin:
Logical Matrix Generation and Testing. 685-693 - Rakesh M. Verma
Optimal Time Bounds for Parallel Term Matching. 694-703
Session 20
- William McCune:
Challenge Equality Problems in Lattice Theory. 704-709 - Frank Pfenning:
Single Axioms in the Implicational Propositional Calculus. 710-713 - Larry Wos, William McCune:
Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. 714-729 - Rick L. Stevens:
Challenge Problems from Nonassociative Rings for Theorem Provers. 730-734
System Abstracts
- Matt Kaufmann:
An Interactive Enhancement to the Boyer-Moore Theorem Prover. 735-736 - David A. Plaisted:
A Goal Directed Theorem Prover. 737 - Bill Pase, Sentot Kromodimoeljo:
m-NEVER System Summary. 738-739 - Timothy Griffin:
EFS - An Interactive Environment for Formal Systems. 740-741 - David A. McAllester:
Ontic: A Knowledge Representation System for Mathematics. 742-743 - Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade:
Some Tools for an Inference Laboratory (ATINF). 744-745 - V. S. Subrahmanian, Zerksis D. Umrigar:
QUANTLOG: A System for Approximate Reasoning in Inconsistent Formal Systems. 746-747 - Stephen J. Garland, John V. Guttag:
LP: The Larch Prover. 748-749 - Mark E. Stickel:
The KLAUS Automated Deduction System. 750-751 - Mark E. Stickel:
A Prolog Technology Theorem Prover. 752-753 - Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller
Lambda-Prolog: An Extended Logic Programming Language. 754-755 - Frank M. Brown, Seung S. Park:
SYMEVAL: A Theorem Prover Based on the Experimental Logic. 756-757 - Frank M. Brown, Seung S. Park, Jim Phelps:
ZPLAN: An Automatic Reasoning System for Situations. 758-759 - Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning:
The TPS Theorem Proving System. 760-761 - Pierre Bieber, Luis Fariñas del Cerro, Andreas Herzig:
MOLOG: a Modal PROLOG. 762-763 - P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov:
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. 764-765 - Bruce T. Smith, Donald W. Loveland:
An nH-Prolog Implementation. 766-767 - Deepak Kapur, Hantao Zhang:
RRL: A Rewrite Rule Laboratory. 768-769 - David Cyrluk, Richard M. Harris, Deepak Kapur:
GEOMETER: A Theorem Prover for Algebraic Geometry. 770-771 - Lawrence C. Paulson
Isabelle: The Next Seven Hundred Theorem Provers. 772-773 - Mehmet Dincbas, Pascal Van Hentenryck, Helmut Simonis
The CHIP System: Constraint Handling In Prolog. 774-775
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-15 19:47 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: