Skip to main content
SpringerLink
Log in

Relating resolution and algebraic completion for Horn logic

  • Term Rewriting Systems
  • Conference paper
  • First Online:
8th International Conference on Automated Deduction (CADE 1986)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 230))

Included in the following conference series:

Abstract

Since first order logic and, especially, Horn logic is used as a programming language, the most common interpretation method for such programs is resolution. Algebraic completion and term rewriting techniques were recently proposed as an alternative to resolution oriented theorem provers. In this paper, the relation between resolution and algebraic completion (restricted to Horn logic) is closely analysed. It is shown, that both methods are equivalent in terms of inference steps and unifications, and, that using the completion method for interpreting (Horn) logic programs, no efficiency can be gained as compared with resolution.

This work has been done within a joint project of the GMD and the SFB 314 (artificial intelligence) at the University of Karlsruhe

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Benanav, D. Kapur, P. Narendran: Complexity of Matching Problems, 1st Int. Conf. on Term Rewriting Techniques and Applications, Dijon, France, Springer LNCS 202, 1985.

    Google Scholar 

  2. W. F. Clocksin, C. S. Mellish: Programming in Prolog, Springer, 1981.

    Google Scholar 

  3. N. Dershowitz, N. A. Josephson: Logic Programming by Completion, Proc. 2nd Int. Logic Programming Conf., Uppsala, 1985.

    Google Scholar 

  4. P. Deussen: Control of and Algorithms for Reduction systems, Unpublished report, University of Karlsruhe, Institut für Informatik I, 1983.

    Google Scholar 

  5. P. Deussen: Private Communication, 1985.

    Google Scholar 

  6. R. Dietrich: Relating Resolution and Algebraic Completion for Horn Logic, Arbeitspapiere der GMD Nr. 177, Gesellschaft für Mathematik und Datenverarbeitung mbH, Bonn, 1985.

    Google Scholar 

  7. J. A. Goguen, J. Meseguer: Equality, Types, Modules and (Why not?) Generics for Logic Programming, J. Logic Programming 1984, 2: 179–210.

    Article  Google Scholar 

  8. A. Herold: Some Basic Notions of First-Order Unification Theory, Universität Karlsruhe, Fakultät für Informatik, Interner Bericht Nr. 15/83, 1983.

    Google Scholar 

  9. J. Hsiang, N. Dershowitz: Rewrite Methods for Clausal and Non-Clausal Theorem Proving, Proc. 10th Int. Conf. on Automata, Languages and Programming, Springer LNCS 154, 1983.

    Google Scholar 

  10. J. Hsiang: Topics in Automated Theorem Proving and Program Generation, Ph. D. Thesis, University of Illinois at Urbana-Champaign, 1983.

    Google Scholar 

  11. J. Hsiang: Two Results in Term Rewriting Theorem Proving, 1st Int. Conf. on Term Rewriting Techniques and Applications, Dijon, France, Springer LNCS 202, 1985.

    Google Scholar 

  12. G. Huet: Confluent Reductions: Abstract Properties and Application to Term Rewriting Systems, JACM, Vol. 27, No. 4, October 1980.

    Google Scholar 

  13. G. Huet, D. C. Oppen: Equations and Rewrite Rules: A survey, R. Book (Ed.): Formal Language Theory. Perspectives and Open Problems. Academic Press, 1980.

    Google Scholar 

  14. J.-M. Hullot: Canonical Forms and Unification, Proc. 5th Int. Conf. on Automated Deduction, Springer LNCS 87, 1980.

    Google Scholar 

  15. D. Kapur, P. Narendran: An Equational Approach to Theorem Proving in First-Order Predicate Calculus, Proc. IJCAI 85, Los Angeles, 1985.

    Google Scholar 

  16. D. E. Knuth, P. B. Bendix: Simple Word Problems in Universal Algebra, J. Leech (Ed.): Computational Problems in Universal Algebra, Pergamon Press, 1970.

    Google Scholar 

  17. J. W. Lloyd: Foundations of Logic Programming, Springer, 1984.

    Google Scholar 

  18. D. W. Loveland: Automated Theorem Proving: A Logical Basis, North-Holland, 1978.

    Google Scholar 

  19. N. J. Nilsson: Principles of Artificial Intelligence, Springer, 1982.

    Google Scholar 

  20. D. A. Waterman, F. Hayes-Roth (Eds.): Pattern Directed Inference Systems, Academic Press, 1978.

    Google Scholar 

  21. E. Paul: A New Interpretation of the Resolution Principle, Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS 170, 1984.

    Google Scholar 

  22. J. A. Robinson: A Machine Oriented Logic Based on the Resolution Principle, JACM, Vol 12, No. 1, January 1965, pp. 23–41.

    Article  Google Scholar 

  23. J. R. Slagle: Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity, JACM, Vol 21, No. 4, October 1974, pp. 622–642.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. GMD Research Laboratory at the University of Karlsruhe, Haid-und-Neu-Straße 7, D 7500, Karlsruhe 1, Germany (West)

    Roland Dietrich

Authors
  1. Roland Dietrich
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jörg H. Siekmann

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dietrich, R. (1986). Relating resolution and algebraic completion for Horn logic. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_80

Download citation

  • DOI: https://doi.org/10.1007/3-540-16780-3_80

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16780-8

  • Online ISBN: 978-3-540-39861-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation