## Donald W. Loveland

*Proceedings of the Sixth International Conference on Automated Deduction*

CADE, 1982.

@proceedings{CADE-1982, address = "6th Conference on Automated Deduction, New York, USA", editor = "Donald W. Loveland", isbn = "3-540-11558-7", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Sixth International Conference on Automated Deduction}", volume = 138, year = 1982, }

### Contents (23 items)

- CADE-1982-Wos #automation
- Solving Open Questions with an Automated Theorem-Proving Program (LW), pp. 1–31.
- CADE-1982-ShostakSM #logic #named #specification #verification
- STP: A Mechanized Logic for Specification and Verification (RES, RLS, PMMS), pp. 32–49.
- CADE-1982-MillerCA
- A Look at TPS (DM, ELC, PBA), pp. 50–69.
- CADE-1982-LuskMO #architecture #kernel #logic
- Logic Machine Architecture: Kernel Funtions (ELL, WM, RAO), pp. 70–84.
- CADE-1982-LuskMO82a #architecture #logic
- Logic Machine Architecture: Inference Mechanisms (ELL, WM, RAO), pp. 85–108.
- CADE-1982-WinkerW #implementation
- Procedure Implementation Through Demodulation and Related Tricks (SKW, LW), pp. 109–131.
- CADE-1982-Silver #equation
- The Application of Homogenization to Simultaneous Equations (BS), pp. 132–143.
- CADE-1982-SterlingB #verification
- Meta-Level Inference and Program Verification (LS, AB), pp. 144–150.
- CADE-1982-Weyhrauch #using
- An Example of FOL Using Metatheory (RWW), pp. 151–158.
- CADE-1982-GreenbaumNOP #comparison #deduction #implementation
- Comparison of Natural Deduction and Locking Resolution Implementations (SG, AN, PO, DAP), pp. 159–171.
- CADE-1982-Smith #synthesis
- Derived Preconditions and Their Use in Program Synthesis (DRS), pp. 172–193.
- CADE-1982-Goad #automation #source code
- Automatic Construction of Special Purpose Programs (CG), pp. 194–208.
- CADE-1982-Shostak
- Deciding Combinations of Theories (RES), pp. 209–222.
- CADE-1982-PietrzykowskiM #backtracking #deduction #exponential #performance
- Exponential Improvement of Efficient Backtracking: A Strategy for Plan-Based Deduction (TP, SM), pp. 223–239.
- CADE-1982-MatwinP #backtracking #data type #exponential #implementation #performance
- Exponential Improvement of Efficient Backtracking: data Structure and Implementation (SM, TP), pp. 240–259.
- CADE-1982-Gabbay #logic
- Intuitonistic Basis for Non-Monotonic Logic (DMG), pp. 260–273.
- CADE-1982-FrischA #retrieval
- Knowledge Retrieval as Limited Inference (AMF, JFA), pp. 274–291.
- CADE-1982-Minker #database #on the
- On Indefinite Databases and the Closed World Assumption (JM), pp. 292–308.
- CADE-1982-Caferra #matrix #proving #reduction #validation
- Proof by Matrix Reduction as Plan + Validation (RC), pp. 309–325.
- CADE-1982-HornigB #algorithm
- Improvements of a Tautology-Testing Algorithm (KMH, WB), pp. 326–341.
- CADE-1982-HenschenN #database #first-order #infinity #recursion #representation #sequence
- Representing Infinite Sequences of Resolvents in recursive First-Order Horn Databases (LJH, SAN), pp. 342–359.
- CADE-1982-Book #power of #string #term rewriting
- The Power of the Church-Rosser Property for String Rewriting Systems (RVB), pp. 360–368.
- CADE-1982-SiekmannS #classification #equation #unification
- Universal Unification and a Classification of Equational Theories (JHS, PS), pp. 369–389.

4 ×#logic

3 ×#implementation

2 ×#architecture

2 ×#automation

2 ×#backtracking

2 ×#database

2 ×#deduction

2 ×#equation

2 ×#exponential

2 ×#performance

3 ×#implementation

2 ×#architecture

2 ×#automation

2 ×#backtracking

2 ×#database

2 ×#deduction

2 ×#equation

2 ×#exponential

2 ×#performance