default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID8th CADE 1986: Oxford, England
- Jörg H. Siekmann:
8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings. Lecture Notes in Computer Science 230, Springer 1986, ISBN 3-540-16780-3
Invited Talk
- Peter B. Andrews:
Connections and Higher-Order Logic. 1-4
Term Rewriting Systems
- Leo Bachmair, Nachum Dershowitz:
Commutation, Transformation, and Termination. 5-20 - Sara Porat, Nissim Francez:
Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems. 21-41 - Ahlem Ben Cherifa, Pierre Lescanne:
An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations. 42-51 - Isabelle Gnaedig, Pierre Lescanne:
Proving Termination of Associative Commutative Rewriting Systems by Rewriting. 52-61 - Roland Dietrich:
Relating Resolution and Algebraic Completion for Horn Logic. 62-78 - David A. Plaisted:
A Simple Non-Termination Test for the Knuth-Bendix Method. 79-88 - Rafael Dueire Lins:
A New Formula for the Execution of Categorial Combinators. 89-98 - Deepak Kapur, Paliath Narendran, Hantao Zhang:
Proof by Induction Using Test Sets. 99-117 - Yoshihito Toyama:
How to Prove Equivalence of Term Rewriting Systems without Induction. 118-127 - Hubert Comon:
Sufficient Completness, Term Rewriting Systems and "Anti-Unification". 128-140 - Jieh Hsiang, Michaël Rusinowitch:
A New Method for Establishing Refutational Completeness in Theorem Proving. 141-152
Nonclassical Deduction
- Gerhard Jäger:
Some Contributions to the Logical Analysis of Circumscrition. 154-171 - Martín Abadi, Zohar Manna:
Modal Theorem Proving. 172-189 - Peter H. Schmitt:
Computational Aspects of Three-Valued Logic. 190-198 - Kurt Konolige:
Resolution and Quantified Epistemic Logics. 199-208 - Frank M. Brown:
A Commonsense Theory of Nonmonotonic Reasoning. 209-228
Equality Reasoning
- Larry Wos, William McCune:
Negative Paramodulation. 229-239 - Younghwan Lim:
The Heuristics and Experimental Results of a New Hyperparamodulation: HL-Resolution. 240-253 - Tie-Cheng Wang:
ECR: An Equality Conditional Resolution Proof Procedure. 254-271 - A. J. J. Dick, Jim Cunningham:
Using Narrowing to do Isolation in Symbolic Equation Solving - An Experiment in Automated Reasoning. 272-280
Program Verification
- Tadashi Kanamori, Hiroshi Fujita:
Formulation of Induction Formulas in Verification of Prolog Programs. 281-299 - Thomas Käufl:
Program Verifier "Tatzelwurm": Reasoning about Systems of Linear Inequalities. 300-305 - Reiner Hähnle
, Maritta Heisel, Wolfgang Reif, Werner Stephan:
An Interactive Verification System Based on Dynamic Logic. 306-315
Graph Based Deduction
- Norbert Eisinger:
What You Always Wanted to Know About Clause Graph Resolution. 316-336 - Rasiah Loganantharaj, Robert A. Mueller:
Parallel Theorem Proving with Connection Graphs. 337-352 - Neil V. Murray, Erik Rosenthal:
Theory Links in Semantic Graphs. 353-364
Special Deduction Systems
- David A. Plaisted:
Abstraction Using Generalization Functions. 365-376 - Hans-Albert Schneider:
An Improvement of Deduction Plans: Refutation Plans. 377-383 - Franz Oppacher, E. Suen:
Controlling Deduction with Proof Condensation and Heuristics. 384-393 - Jonathan Traugott:
Nested Resolution. 394-402
Invited Talk
- Gérard P. Huet:
Mechanizing Constructive Proofs (Abstract). 403
Constructive ATP
- Douglas J. Howe:
Implementing Number Theory: An Experiment with Nuprl. 404-415
Unification Theory
- Cynthia Dwork, Paris C. Kanellakis, Larry J. Stockmeyer:
Parallel Algorithms for Term Matching. 416-430 - Erik Tidén:
Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols. 431-449 - Alexander Herold:
Combination of Unification Algorithms. 450-469 - Wolfram Büttner:
Unification in the Data Structure Sets. 470-488 - Deepak Kapur, Paliath Narendran:
NP-Completeness of the Set Unification and Matching Problems. 489-495 - Jalel Mzali:
Matching with Distributivity. 496-505 - Ursula Martin, Tobias Nipkow:
Unification in Boolean Rings. 506-513 - Hans-Jürgen Bürckert:
Some Relationships between Unification, restricted Unification, and Matching. 514-524 - Christoph Walther:
A Classification of Many-Sorted Unification Problems. 525-537 - Manfred Schmidt-Schauß:
Unification in Many-Sorted Eqational Theories. 538-552
Theoretical Issues
- Hans Kleine Büning, Theodor Lettmann:
Classes of First Order Formulas Under Various Satisfiability Definitions. 553-563 - Volker Weispfenning:
Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs. 564-571
Logic Programming Oriented Deduction Systems
- Mark E. Stickel:
A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. 573-587 - Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek:
Paths to High-Performance Automated Theorem Proving. 588-597 - F. Keith Hanna, Neil Daeche:
Purely Functional Implementation of a Logic. 598-607
Deductive Databases, Planning, Synthesis
- Philip T. Cox, Tomasz Pietrzykowski:
Causes for Events: Their Computation and Applications. 608-621 - Zohar Manna, Richard J. Waldinger:
How to Clear a Block: Plan Formation in Situational Logic. 622-640 - Jonathan Traugott:
Deductive Synthesis of Sorting Programs. 641-660
Extended Abstracts of Courrent Deduction Systems
- Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper:
The TPS Theorem Proving System. 663-664 - Jürgen Avenhaus, Benjamin Benninghofen, Rüdiger Göbel, Klaus Madlener:
TRSPEC: A Term Rewriting Based System for Algebraic Specifications. 665-667 - M. Bayerl:
Highly Parallel Inference Machine. 668-669 - Christoph Beierle, Walter G. Olthoff, Angi Voß:
Automatic Theorem Proving in the ISDV System. 670-671 - Susanne Biundo, Birgit Hummel, Dieter Hutter, Christoph Walther:
The Karlsruhe Induction Theorem Proving System. 672-674 - Robert S. Boyer, J Strother Moore:
Overview of a Theorem-Prover for A Computational Logic. 675-678 - Shang-Ching Chou:
GEO-Prover - A Geometry Theorem Prover Developed at UT. 679-680 - Norbert Eisinger, Hans Jürgen Ohlbach:
The Markgraf Karl Refutation Procedure (MKRP). 681-682 - Jacek Gibert:
The J-Machine: Functional Programming with Combinators. 683-684 - Steven Greenbaum, David A. Plaisted:
The Illinois Prover: A General Purpose Resolution Theorem Prover. 685-687 - Gérard P. Huet:
Theorem Proving Systems of the Formel Project. 687-688 - Heinrich Hußmann:
The Passau RAP System: Prototyping Algebraic Specifications Using Conditional Narrowing. 689-690 - Deepak Kapur, G. Sivakumar, Hantao Zhang:
RRL: A Rewrite Rule Laboratory. 691-692 - B. Kutzler, Sabine Stifter:
A Geometry Theorem Prover Based on Buchberger's Algorithm. 693-694 - Pierre Lescanne:
REVE a Rewrite Rule Laboratory. 695-696 - Ewing L. Lusk, William McCune, Ross A. Overbeek:
ITP at Argonne National Laboratory. 697-698 - Charles G. Morgan:
AUTOLOGIC at University of Victoria. 699-700 - Francis Jeffry Pelletier:
THINKER. 701-702 - Mark E. Stickel:
The KLAUS Automated Deduction System. 703-704 - Paul B. Thistlewaite, Michael A. McRobbie, Robert K. Meyer:
The KRIPKE Automated Theorem Proving System. 705-706 - Tie-Cheng Wang:
SHD-Prover at University of Texas at Austin. 707-708
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 2026-01-28 00:26 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:
