Skip to main content
SpringerLink
Log in

A maximal-literal unit strategy for horn clauses

  • Chapter 1 Theory Of Conditional And Horn Clause Systems
  • Conference paper
  • First Online:
Conditional and Typed Rewriting Systems (CTRS 1990)

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

Included in the following conference series:

Abstract

A new positive-unit theorem-proving procedure for equational Horn clauses is presented. It uses a term ordering to restrict paramodulation to potentially maximal sides of equations. Completeness is shown using proof orderings.

This research supported in part by the National Science Foundation under Grant CCR-9007195.

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. L. Bachmair, Canonical Equational Proofs. Boston: Birkhäuser, 1991. To appear.

    Google Scholar 

  2. L. Bachmair, N. Dershowitz, and J. Hsiang, “Orderings for equational proofs,” in Proceedings of the IEEE Symposium on Logic in Computer Science, (Cambridge, MA), pp. 346–357, June 1986.

    Google Scholar 

  3. L. Bachmair, N. Dershowitz, and D. A. Plaisted, “Completion without failure,” in Resolution of Equations in Algebraic Structures 2: Rewriting Techniques (H. Aït-Kaci and M. Nivat, eds.), ch. 1, pp. 1–30, New York: Academic Press, 1989.

    Google Scholar 

  4. L. Bachmair and H. Ganzinger,. “On restrictions of ordered paramodulation with simplification,” in Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems (M. Okada, ed.), (Montreal, Canada), June 1990. Lecture Notes in Computer Science, Springer, Berlin.

    Google Scholar 

  5. R. S. Boyer, Locking: A restriction of resolution. PhD thesis, University of Texas at Austin, Austin, TX, 1971.

    Google Scholar 

  6. T. C. Brown, Jr., A structured design-method for specialized proof procedures. PhD thesis, California Institute of Technology, Pasadena, CA, 1975.

    Google Scholar 

  7. H. Comon, “Solving inequations in term algebras (Preliminary version),” in Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (Philadelphia, PA), pp. 62–69, June 1990.

    Google Scholar 

  8. N. Dershowitz, “Orderings for term-rewriting systems,” Theoretical Computer Science, vol. 17, pp. 279–301, March 1982.

    Google Scholar 

  9. N. Dershowitz, “Termination of rewriting,” J. of Symbolic Computation, vol. 3, pp. 69–115, February/April 1987. Corrigendum: 4, 3 (December 1987), 409–410.

    Google Scholar 

  10. N. Dershowitz and J.-P. Jouannaud, “Rewrite systems,” in Handbook of Theoretical Computer Science B: Formal Methods and Semantics, (J. van Leeuwen, ed.), ch. 6, Amsterdam: North-Holland, 1990.

    Google Scholar 

  11. N. Dershowitz and Z. Manna, “Proving termination with multiset orderings,” Communications of the ACM, vol. 22, pp. 465–476, August 1979.

    Google Scholar 

  12. N. Dershowitz and M. Okada, “Proof-theoretic techniques and the theory of rewriting,” in Proceedings of the Third IEEE Symposium on Logic in Computer Science (Edinburgh, Scotland), pp. 104–111, July 1988.

    Google Scholar 

  13. N. Dershowitz and M. Okada, “A rationale for conditional equational programming,” Theoretical Computer Science, vol. 75, pp. 111–138, 1990.

    Google Scholar 

  14. U. Furbach, “Oldy but goody: Paramodulation revisited,” in Proceedings of the GI Workshop on Artificial Intelligence (Morik, ed.), pp. 195–200, 1987. Vol. 152 of Informatik Fachberichte.

    Google Scholar 

  15. H. Ganzinger, “A completion procedure for conditional equations,” in Proceedings of the First International Workshop on Conditional Term Rewriting Systems (S. Kaplan and J.-P. Jouannaud, eds.), (Orsay, France), pp. 62–83, July 1987. Vol. 308 of Lecture Notes in Computer Science, Springer, Berlin (1988).

    Google Scholar 

  16. L. Henschen and L. Wos, “Unit refutations and Horn sets,” J. of the Association for Computing Machinery, vol. 21, pp. 590–605, 1974.

    Google Scholar 

  17. J. Hsiang and M. Rusinowitch, “A new method for establishing refutational completeness in theorem proving,” in Proceedings of the Eighth International Conference on Automated Deduction (J. H. Siekmann, ed.), (Oxford, England), pp. 141–152, July 1986. Vol. 230 of Lecture Notes in Computer Science, Springer, Berlin.

    Google Scholar 

  18. J. Hsiang and M. Rusinowitch, “On word problems in equational theories,” in Proceedings of the Fourteenth EATCS International Conference on Automata, Languages and Programming (T. Ottmann, ed.), (Karlsruhe, West Germany), pp. 54–71, July 1987. Vol. 267 of Lecture Notes in Computer Science, Springer, Berlin.

    Google Scholar 

  19. S. Kamin and J.-J. Lévy, “Two generalizations of the recursive path ordering,” Unpublished note, Department of Computer Science, University of Illinois, Urbana, IL, February 1980.

    Google Scholar 

  20. S. Kaplan, “Simplifying conditional term rewriting systems: Unification, termination and confluence,” J. of Symbolic Computation, vol. 4, pp. 295–334, December 1987.

    Google Scholar 

  21. D. E. Knuth and P. B. Bendix, “Simple word problems in universal algebras,” in Computational Problems in Abstract Algebra (J. Leech, ed.), pp. 263–297, Oxford, U. K.: Pergamon Press, 1970. Reprinted in Automation of Reasoning 2, Springer, Berlin, pp. 342–376 (1983).

    Google Scholar 

  22. E. Kounalis and M. Rusinowitch, “On word problems in Horn theories,” in Proceedings of the First International Workshop on Conditional Term Rewriting Systems (S. Kaplan and J.-P. Jouannaud, eds.), (Orsay, France), pp. 144–160, July 1987. Vol. 308 of Lecture Notes in Computer Science, Springer, Berlin (1988).

    Google Scholar 

  23. D. S. Lankford, “Canonical inference,” Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX, December 1975.

    Google Scholar 

  24. E. Paul, “On solving the equality problem in theories defined by Horn clauses,” Theoretical Computer Science, vol. 44, no. 2, pp. 127–153, 1986.

    Google Scholar 

  25. G. Robinson and L. Wos, “Paramodulation and theorem-proving in first order theories with equality,” in Machine Intelligence 4 (B. Meltzer and D. Michie, eds.), pp. 135–150, Edinburgh, Scotland: Edinburgh University Press, 1969.

    Google Scholar 

  26. M. Rusinowitch, Démonstration Automatique: Techniques de réécriture. Paris, France: InterEditions, 1989.

    Google Scholar 

  27. G. Sivakumar, Proofs and Computations in Conditional Equational Theories. PhD thesis, Department of Computer Science, University of Illinois, Urbana, IL, 1989.

    Google Scholar 

  28. H. Zhang and D. Kapur, “First-order theorem proving using conditional equations,” in Proceedings of the Ninth International Conference on Automated Deduction (E. Lusk and R. Overbeek, eds.), (Argonne, Illinois), pp. 1–20, May 1988. Vol. 310 of Lecture Notes in Computer Science, Springer, Berlin.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois at Urbana-Champaign, 1304 West Springfield Avenue, 61801, Urbana, IL, U.S.A.

    Nachum Dershowitz

Authors
  1. Nachum Dershowitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Kaplan M. Okada

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dershowitz, N. (1991). A maximal-literal unit strategy for horn clauses. In: Kaplan, S., Okada, M. (eds) Conditional and Typed Rewriting Systems. CTRS 1990. Lecture Notes in Computer Science, vol 516. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54317-1_78

Download citation

  • DOI: https://doi.org/10.1007/3-540-54317-1_78

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54317-6

  • Online ISBN: 978-3-540-47558-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation