[go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Canonical Ground Horn Theories

  • Chapter
Programming Logics

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7797))

Abstract

An abstract framework of canonical inference based on proof orderings is applied to ground Horn theories with equality. A finite presentation that makes all normal-form proofs available is called saturated. To maximize the chance that a saturated presentation be finite, it should also be contracted, in which case it is deemed canonical. We apply these notions to propositional Horn theories – or equivalently Moore families – presented as implicational systems or associative-commutative rewrite systems, and ground equational Horn theories, presented as decreasing conditional rewrite systems. For implicational systems, we study different notions of optimality and the completion procedures that generate them, and we suggest a new notion of rewrite-optimality, that takes contraction by simplification into account. For conditional rewrite systems, we show that reduced (fully normalized) is stronger than contracted (sans redundancy), and accordingly the perfect system – complete and reduced – is preferred to the canonical one – saturated and contracted. We conclude with a survey of approaches to normal-form proofs, saturated, or canonical, systems, and decision procedures based on them.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Apt, K.R.: Logic programming. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, vol. B, ch. 10, pp. 493–574. North-Holland, Amsterdam (1990)

    Google Scholar 

  2. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic 10(1), 129–179 (2009)

    Article  MathSciNet  Google Scholar 

  3. Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation 183(2), 140–164 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bachmair, L., Dershowitz, N.: Inference rules for rewrite-based first-order theorem proving. In: Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, pp. 331–337. IEEE Computer Society Press (1987)

    Google Scholar 

  5. Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. Journal of the Association for Computing Machinery 41(2), 236–276 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Aït-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol. II, pp. 1–30. Academic Press (1989)

    Google Scholar 

  7. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4, 217–247 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  8. Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. Journal of Automated Reasoning 31(2), 129–168 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  9. Baumgartner, P. (ed.): Theory Reasoning in Connection Calculi. LNCS (LNAI), vol. 1527. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  10. Bertet, K., Monjardet, B.: The multiple facets of the canonical direct implicational basis. Cahiers de la MSE No. b05052, Maison des Sciences Economiques, Université Paris Panthéon-Sorbonne (June 2005), http://ideas.repec.org/p/mse/wpsorb/b05052.html

  11. Bertet, K., Nebut, M.: Efficient algorithms on the Moore family associated to an implicational system. Discrete Mathematics and Theoretical Computer Science 6, 315–338 (2004)

    MathSciNet  MATH  Google Scholar 

  12. Birkhoff, G.: Lattice Theory. Revised edn. American Mathematical Society, New York (1948)

    Google Scholar 

  13. Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Transactions on Computational Logic 8(1) (2007)

    Google Scholar 

  14. Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. In: Cook, B., Sebastiani, R. (eds.) Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Fourth Federated Logic Conference (FLoC). Electronic Notes in Theoretical Computer Science, vol. 174(8), pp. 55–70. Elsevier, Amsterdam (2007)

    Google Scholar 

  15. Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial T-satisfiability procedures. Journal of Logic and Computation 18(1), 77–96 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  16. Bonacina, M.P., Echenim, M.: Theory decision by decomposition. Journal of Symbolic Computation 45(2), 229–260 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  17. Bonacina, M.P., Hsiang, J.: On rewrite programs: Semantics and relationship with Prolog. Journal of Logic Programming 14(1 & 2), 155–180 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  18. Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoretical Computer Science 146, 199–242 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  19. Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. Journal of Automated Reasoning 47(2), 161–189 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  20. Brown Jr., T.C.: A Structured Design-Method for Specialized Proof Procedures. PhD thesis, California Institute of Technology, Pasadena, CA (1975)

    Google Scholar 

  21. Burel, G., Kirchner, C.: Completion Is an Instance of Abstract Canonical System Inference. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Goguen Festschrift 2006. LNCS, vol. 4060, pp. 497–520. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Caspard, N., Monjardet, B.: The lattice of Moore families and closure operators on a finite set: A survey. Electronic Notes in Discrete Mathematic, vol. 2 (1999)

    Google Scholar 

  23. Chang, C.L., Lee, R.C.T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press (1973)

    Google Scholar 

  24. Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2005), http://www.grappa.univ-lille3.fr/tata

  25. Comon-Lundh, H., Courtier, V.: New Decidability Results for Fragments of First-order Logic and Application to Cryptographic Protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 148–164. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  26. Dershowitz, N.: A note on simplification orderings. Information Processing Letters 9(5), 212–215 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  27. Dershowitz, N.: Equations as programming language. In: Proceedings of the Fourth Jerusalem Conference on Information Technology, Jerusalem, Israel, pp. 114–124. IEEE Computer Society Press (May 1984)

    Google Scholar 

  28. Dershowitz, N.: Computing with rewrite systems. Information and Control 64(2/3), 122–157 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  29. Dershowitz, N.: Canonical Sets of Horn Clauses. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 267–278. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  30. Dershowitz, N.: Ordering-based strategies for Horn clauses. In: Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, Sydney, Australia, pp. 118–124 (1991)

    Google Scholar 

  31. Dershowitz, N., Huang, G.S., Harris, M.A.: Enumeration problems related to ground Horn theories (2008), http://arxiv.org/abs/cs/0610054

  32. Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, vol. B, ch. 6, pp. 243–320. North-Holland, Amsterdam (1990)

    Google Scholar 

  33. Dershowitz, N., Kirchner, C.: Abstract canonical presentations. Theoretical Computer Science 357, 53–69 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  34. Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  35. Dershowitz, N., Marcus, L., Tarlecki, A.: Existence, uniqueness, and construction of rewrite systems. SIAM Journal of Computing 17(4), 629–639 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  36. Dershowitz, N., Plaisted, D.A.: Logic programming cum applicative programming. In: Proceedings of the 1985 Symposium on Logic Programming, Boston, MA, pp. 54–66 (1985)

    Google Scholar 

  37. Dershowitz, N., Plaisted, D.A.: Equational programming. In: Hayes, J.E., Michie, D., Richards, J. (eds.) Machine Intelligence 11: The Logic and Acquisition of Knowledge, ch. 2, pp. 21–56. Oxford University Press, Oxford (1988)

    Google Scholar 

  38. Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 9, pp. 535–610. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  39. Dershowitz, N., Reddy, U.: Deductive and inductive synthesis of equational programs. Journal of Symbolic Computation 15, 467–494 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  40. Dowek, G.: Confluence as a Cut Elimination Property. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 2–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  41. Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulæ. Journal of Logic Programming 1(3), 267–284 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  42. Fermüller, C., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, ch. 25, pp. 1793–1849. Elsevier, Amsterdam (2001)

    Google Scholar 

  43. Fribourg, L.: Slog—Logic Interpreter for Equational Clauses. In: Choffrut, C., Lengauer, T. (eds.) STACS 1990. LNCS, vol. 415, pp. 479–480. Springer, Heidelberg (1990)

    Google Scholar 

  44. Furbach, U., Obermaier, C.: Knowledge compilation for description logics. In: Dershowitz, N., Voronkov, A. (eds.) Proceedings of the Fourteenth International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Short Papers Session (2007)

    Google Scholar 

  45. Gallier, J., Narendran, P., Plaisted, D.A., Raatz, S., Snyder, W.: Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time. Journal of the Association for Computing Machinery 40(1), 1–16 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  46. Gallier, J.H.: Fast algorithms for testing unsatisfiability of ground Horn clauses with equations. Journal of Symbolic Computation 4, 233–254 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  47. Ganzinger, H.: A completion procedure for conditional equations. Journal of Symbolic Computation 11(1 & 2), 51–81 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  48. Goguen, J.A., Meseguer, J.: Eqlog: Equality, types, and generic modules for logic programming. In: DeGroot, D., Lindstrom, G. (eds.) Logic Programming: Functions, Relations, and Equations, pp. 295–363. Prentice-Hall, Englewood Cliffs (1986)

    Google Scholar 

  49. Hanus, M.: The integration of functions into logic programming: From theory to practice. Journal of Logic Programming 19&20, 583–628 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  50. Hodges, W.: Logical features of Horn clauses. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Logical Foundations, vol. I, pp. 449–503. Oxford University Press, Oxford (1993)

    Google Scholar 

  51. Horn, A.: On sentences which are true in direct unions of algebras. Journal of Symbolic Logic 16, 14–21 (1951)

    Article  MathSciNet  MATH  Google Scholar 

  52. Hsiang, J.: Refutational theorem proving using term rewriting systems. Artificial Intelligence 25, 255–300 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  53. Hsiang, J.: Rewrite method for theorem proving in first order theories with equality. Journal of Symbolic Computation 3, 133–151 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  54. Hsiang, J., Rusinowitch, M.: On Word Problems in Equational Theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 54–71. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  55. Huet, G.: A complete proof of correctness of the Knuth–Bendix completion algorithm. Journal of Computer and System Sciences 23(1), 11–21 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  56. Jouannaud, J.P., Waldmann, B.: Reductive conditional term rewriting systems. In: Proceedings of the Third IFIP Working Conference on Formal Description of Programming Concepts, Ebberup, Denmark (1986)

    Google Scholar 

  57. Kaplan, S.: Simplifying conditional term rewriting systems: Unification, termination, and confluence. Journal of Symbolic Computation 4(3), 295–334 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  58. Kaplan, S., Rémy, J.L.: Completion algorithms for conditional rewriting systems. In: Aït-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol. II, pp. 141–170. Academic Press (1989)

    Google Scholar 

  59. Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)

    Chapter  Google Scholar 

  60. Kounalis, E., Rusinowitch, M.: On word problems in Horn theories. Journal of Symbolic Computation 11(1 & 2), 113–128 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  61. Lankford, D.S.: Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX (1975)

    Google Scholar 

  62. Lloyd, J.W.: Foundations of Logic Programming, 2nd extended edn. Symbolic Computation Series. Springer, Berlin (1987)

    Google Scholar 

  63. Lynch, C., Morawska, B.: Automatic decidability. In: Plotkin, G. (ed.) Proceedings of the Seventeenth IEEE Symposium in Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  64. McCharen, J.D., Overbeek, R.A., Wos, L.: Complexity and related enhancements for automated theorem proving programs. Computers and Mathematics with Applications 2(1), 1–16 (1976)

    Article  MATH  Google Scholar 

  65. McKinsey, J.C.C.: The decision problem for some classes of sentences without quantifiers. Journal of Symbolic Logic 8, 61–76 (1943)

    Article  MathSciNet  MATH  Google Scholar 

  66. Plaisted, D.A., Sattler-Klein, A.: Proof lengths for equational completion. Information and Computation 125(2), 154–170 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  67. Reddy, U.S.: Narrowing as the operational semantics of functional languages. In: Proceedings of the Symposium on Logic Programming, pp. 138–151. IEEE Computer Society Press (1985)

    Google Scholar 

  68. Roussel, O., Mathieu, P.: Exact Knowledge Compilation in Predicate Calculus: The Partial Achievement Case. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 161–175. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  69. Sloane, N.J.A.: The On-Line Encyclopedia of Integer Sequences (2006), http://www.research.att.com/~njas/sequences

  70. Stickel, M.E.: Automated deduction by theory resolution. Journal of Automated Reasoning 1, 333–355 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  71. Bezem, M., Klop, J.W., de Vrijer, R.: TeReSe: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  72. Wos, L., Carson, D.F., Robinson, G.A.: Efficiency and completeness of the set of support strategy in theorem proving. Journal of the Association for Computing Machinery 12, 536–541 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  73. Zhang, H.: A new method for the boolean ring based theorem proving. Journal of Symbolic Computation 17(2), 189–211 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  74. Zhang, H.: Contextual rewriting in automated reasoning. Fundamenta Informaticae 24, 107–123 (1995)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Verona, Strada Le Grazie 15, I-37134, Verona, Italy

    Maria Paola Bonacina

  2. School of Computer Science, Tel Aviv University, Ramat Aviv, 69978, Israel

    Nachum Dershowitz

Authors
  1. Maria Paola Bonacina
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nachum Dershowitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

  2. Max-Planck-Institut für Informatik, Campus E1 4, 66123, Saarbrücken, Germany

    Christoph Weidenbach

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Bonacina, M.P., Dershowitz, N. (2013). Canonical Ground Horn Theories. In: Voronkov, A., Weidenbach, C. (eds) Programming Logics. Lecture Notes in Computer Science, vol 7797. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37651-1_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-37651-1_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-37650-4

  • Online ISBN: 978-3-642-37651-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation