| Soundness and Completeness of Partial Deductions for Well-Founded Semantics | p. 1 |
| On Deductive Planning and the Frame Problem | p. 13 |
| On Resolution in Fragments of Classical Linear Logic | p. 30 |
| A Procedure for Automatic Proof Nets Construction | p. 42 |
| Free Logic and Infinite Constraint Networks | p. 54 |
| Towards Probabilistic Knowledge Bases | p. 66 |
| Two-Level Grammar: A Functional/Logic Query Language for Database and Knowledge-Base Systems | p. 78 |
| Extending Deductive Database Languages by Embedded Implications | p. 84 |
| Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years | p. 96 |
| Resolution for Many-Valued Logics | p. 107 |
| An Ordered Theory Resolution Calculus | p. 119 |
| Application of Automated Deduction to the Search for Single Axioms for Exponent Groups | p. 131 |
| Elementary Lower Bounds for the Lengths of Refutations | p. 137 |
| Shortening Proofs by Quantifier Introduction | p. 148 |
| Reform Compilation for Nonlinear Recursion | p. 160 |
| Pruning Infinite Failure Branches in Programs with Occur-Check | p. 172 |
| The Use of Planning Critics in Mechanizing Inductive Proofs | p. 178 |
| [lambda][mu]-Calculus: An Algorithmic Interpretation of Classical Natural Deduction | p. 190 |
| Building Proofs by Analogy via the Curry-Howard Isomorphism | p. 202 |
| On the Use of the Constructive Omega-Rule Within Automated Deduction | p. 214 |
| OR-Parallel Theorem Proving with Random Competition | p. 226 |
| Parallel Computation of Multiple Sets-of-Support | p. 238 |
| Towards Using the Andorra Kernel Language for Industrial Real-Time Applications | p. 250 |
| Unification in a Combination of Equational Theories with Shared Constants and its Application to Primal Algebras | p. 261 |
| Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria | p. 273 |
| Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems | p. 285 |
| A Two Step Semantics for Logic Programs with Negation | p. 297 |
| Generalized Negation as Failure and Semantics of Normal Disjunctive Logic Programs | p. 309 |
| General Model Theoretic Semantics for Higher-Order Horn Logic Programming | p. 320 |
| Disjunctive Deductive Databases | p. 332 |
| Netlog - A Concept Oriented Logic Programming Language | p. 357 |
| From the Past to the Future: Executing Temporal Logic Programs | p. 369 |
| Computing Induction Axioms | p. 381 |
| Consistency of Equational Enrichments | p. 393 |
| A Programming Logic for a Verified Structured Assembly Language | p. 403 |
| The Unification of Infinite Sets of Terms and its Applications | p. 409 |
| Unification in Order-Sorted Type Theory | p. 421 |
| Infinite, Canonical String Rewriting Systems Generated by Completion | p. 433 |
| Spes: A System for Logic Program Transformation | p. 445 |
| Linear Objects: A Logic Framework for Open System Programming | p. 448 |
| ISAR: An Interactive System for Algebraic Implementation Proofs | p. 451 |
| Mathpert: Computer Support for Learning Algebra, Trig and Calculus | p. 454 |
| MegaLog - A Platform for Developing Knowledge Base Management Systems | p. 457 |
| SPIKE, an Automatic Theorem Prover | p. 460 |
| An Application to Teaching in Logic Course of ATP Based on Natural Deduction | p. 463 |
| A Generic Logic Environment | p. 466 |
| ElipSys. A Parallel Programming System Based on Logic | p. 469 |
| Opium - A High Level Debugging Environment | p. 472 |
| An Inductive Theorem Prover Based on Narrowing | p. 475 |
| A Cooperative Answering System | p. 478 |
| MIZ-PR: A Theorem Prover for Polymorphic and Recursive Functions | p. 481 |
| ProPre. A Programming Language with Proofs | p. 484 |
| FRIENDLY-WAM: An Interactive Tool to Understand the Compilation of Prolog | p. 487 |
| SEPIA: A Basis for Prolog Extensions | p. 490 |
| The External Database in SICStus Prolog | p. 493 |
| The KCM System: Speeding-up Logic Programming Through Hardware Support | p. 496 |
| Logician's Workbench | p. 499 |
| EUODHILOS: A General Reasoning System for a Variety of Logics | p. 501 |
| The EKS-VI System | p. 504 |
| CHIP and Propia | p. 507 |
| Table of Contents provided by Blackwell. All Rights Reserved. |
