3. LPAR 1992: St. Petersburg, Russia
Non-Resolution Theorem Proving I
Data Bases and Knowledge Bases
: Extending Deductive Database Languages by Embedded Implications.
Resolution Theorem Proving
Ewing L. Lusk
: Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years.
, Larry Wos
: Application of Automated Deduction to the Search for Single Axioms for Exponent Groups.
Theorem Proving and Complexity
: Shortening Proofs by Quantifier Introduction.
: Pruning Infinite Failure Branches in Programs with Occur-Check.
: The Use of Planning Critics in Mechanizing Inductive Proofs.
: Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction.
Parallel Theorem Proving and Logic Programming
: OR-Parallel Theorem Proving with Random Competition.
: Towards Using the Andorra Kernel Language for Industrial Real-Time Applications.
Unification and Equality I
: Unification in a Combination of Equational Theories with Shared Constants and its Application to Primal Algebras.
: Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems.
: Generalized Negation As Failure and Semantics of Normal Disjunctive Logic Programs.
Extensions of Logic Programming
Non-Resolution Theorem Proving II
Specification and Verification
: A Programming Logic for a Verified Structured Assembly Language.
Unification and Equality II
: The Unification of Infinite Sets of Terms and Its Applications.
: Mathpert: Computer Support for Learning Algebra, Trig, and Calculus.
: An Application to Teaching in Logic Course of ATP Based Natural Deduction.
: SEPIA - a Bases for Prolog Extensions.
: The External Database in SICStus Prolog.
: The KCM System: Speeding-up Logic Programming through Hardware Support.