8. CADE 1986:
Oxford, England Jörg H. Siekmann (Ed.):
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
export record as
dblp key:
Term Rewriting Systems
export record as
dblp key:
export record as
dblp key:
Sara Porat ,
Nissim Francez :
Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems.
21-41
export record as
dblp key:
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
export record as
dblp key:
export record as
dblp key:
Roland Dietrich :
Relating Resolution and Algebraic Completion for Horn Logic.
62-78
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
Yoshihito Toyama :
How to Prove Equivalence of Term Rewriting Systems without Induction.
118-127
export record as
dblp key:
Hubert Comon :
Sufficient Completness, Term Rewriting Systems and "Anti-Unification".
128-140
export record as
dblp key:
Nonclassical Deduction
export record as
dblp key:
Gerhard Jäger :
Some Contributions to the Logical Analysis of Circumscrition.
154-171
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
Kurt Konolige :
Resolution and Quantified Epistemic Logics.
199-208
export record as
dblp key:
Frank M. Brown :
A Commonsense Theory of Nonmonotonic Reasoning.
209-228
Equality Reasoning
export record as
dblp key:
export record as
dblp key:
Younghwan Lim :
The Heuristics and Experimental Results of a New Hyperparamodulation: HL-Resolution.
240-253
export record as
dblp key:
Tie-Cheng Wang :
ECR: An Equality Conditional Resolution Proof Procedure.
254-271
export record as
dblp key:
A. J. J. Dick ,
Jim Cunningham :
Using Narrowing to do Isolation in Symbolic Equation Solving - An Experiment in Automated Reasoning.
272-280
Program Verification
export record as
dblp key:
export record as
dblp key:
Thomas Käufl :
Program Verifier "Tatzelwurm": Reasoning about Systems of Linear Inequalities.
300-305
export record as
dblp key:
Graph Based Deduction
export record as
dblp key:
Norbert Eisinger :
What You Always Wanted to Know About Clause Graph Resolution.
316-336
export record as
dblp key:
conf/cade/LoganantharajM86 export record as
dblp key:
Special Deduction Systems
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
Invited Talk
export record as
dblp key:
Constructive ATP
export record as
dblp key:
Douglas J. Howe :
Implementing Number Theory: An Experiment with Nuprl.
404-415
Unification Theory
export record as
dblp key:
export record as
dblp key:
Erik Tidén :
Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols.
431-449
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
Hans-Jürgen Bürckert :
Some Relationships between Unification, restricted Unification, and Matching.
514-524
export record as
dblp key:
export record as
dblp key:
conf/cade/Schmidt-Schauss86
Theoretical Issues
export record as
dblp key:
export record as
dblp key:
Volker Weispfenning :
Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs.
564-571
Logic Programming Oriented Deduction Systems
export record as
dblp key:
Mark E. Stickel :
A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler.
573-587
export record as
dblp key:
export record as
dblp key:
Deductive Databases, Planning, Synthesis
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
Extended Abstracts of Courrent Deduction Systems
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
M. Bayerl :
Highly Parallel Inference Machine.
668-669
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
Shang-Ching Chou :
GEO-Prover - A Geometry Theorem Prover Developed at UT.
679-680
export record as
dblp key:
export record as
dblp key:
Jacek Gibert :
The J-Machine: Functional Programming with Combinators.
683-684
export record as
dblp key:
export record as
dblp key:
Gérard P. Huet :
Theorem Proving Systems of the Formel Project.
687-688
export record as
dblp key:
Heinrich Hußmann :
The Passau RAP System: Prototyping Algebraic Specifications Using Conditional Narrowing.
689-690
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
export record as
dblp key:
conf/cade/ThistlewaiteMM86 export record as
dblp key:
data released under the ODC-BY 1.0 license
