Logic Programming and Automated Reasoning

1. Front Matter

   PDF

2. Soundness and completeness of partial deductions for well-founded semantics

   • Halina Przymusinska, Teodor Przymusinski, Hirohisa Seki

   Pages 1-12

3. On deductive planning and the frame problem

   • Steffen Hölldobler

   Pages 13-29

4. On resolution in fragments of classical linear logic (extended abstract)

   • J. A. Harland, D. J. Pym

   Pages 30-41

5. A procedure for automatic proof nets construction

   • Didier Galmiche, Guy Perrier

   Pages 42-53

6. Free logic and infinite constraint networks

   • James Bowen, Dennis Bahler

   Pages 54-65

7. Towards probabilistic knowledge bases

   • Beat Wüthrich

   Pages 66-77

8. Two-level grammar: A functional/logic query language for database and knowledge-base systems

   • Barrett R. Bryant, Aiqin Pan

   Pages 78-83

9. Extending deductive database languages by embedded implications

   • Burkhard Freitag

   Pages 84-95

10. Controlling redundancy in large search spaces: Argonne-style theorem proving through the years

    • Ewing L. Lusk

    Pages 96-106

11. Resolution for many-valued logics

    • Matthias Baaz, Christian G. Fermüller

    Pages 107-118

12. An ordered theory resolution calculus

    • Peter Baumgartner

    Pages 119-130

13. Application of automated deduction to the search for single axioms for exponent groups

    • William McCune, Larry Wos

    Pages 131-136

14. Elementary lower bounds for the lengths of refutations

    • Hai-Ping Ko, Mark E. Nadel

    Pages 137-147

15. Shortening proofs by quantifier introduction

    • Uwe Egly

    Pages 148-159

16. Reform compilation for nonlinear recursion

    • Håkan Millroth

    Pages 160-171

17. Pruning infinite failure branches in programs with occur-check

    • Ulrich Neumerkel

    Pages 172-177

18. The use of planning critics in mechanizing inductive proofs

    • Andrew Ireland

    Pages 178-189

19. λμ-Calculus: An algorithmic interpretation of classical natural deduction

    • Michel Parigot

    Pages 190-201

20. Building proofs by analogy via the Curry-Howard Isomorphism

    • Thierry Boy de la Tour, Christoph Kreitz

    Pages 202-213

This volume contains the proceedings of LPAR '92, the international conference on logic programming and automated reasoning held in St. Petersburg in July 1992. The aim of the conference was to bring together researchers from the Russian and the international logic programming and theorem proving communities. The topics of interest covered by papers inthe volume include automated theorem proving, non-monotonic reasoning, applications of mathematical logic to computer science, deductive databases, implementation of declarative concepts, and programming in non-classical logics. LPAR '92 is the successor of the First and Second Russian Conferences on Logic Programming held in 1990 and 1991, respectively, the proceedings of which were publishedin LNAI Vol. 592.

• Automat
• artificial intelligence
• automated reasoning
• automated theorem proving
• logic
• nonmonotonic reasoning
• programming
• proving
• theorem proving

Policies and ethics