Document Open Access Logo

Extending Maximal Completion (Invited Talk)

Author Sarah Winkler

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.3.pdf
  • Filesize: 0.49 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • automated reasoning
  • completion
  • theorem proving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Maximal completion (Klein and Hirokawa 2011) is an elegantly simple yet powerful variant of Knuth-Bendix completion. This paper extends the approach to ordered completion and theorem proving as well as normalized completion. An implementation of the different procedures is described, and its practicality is demonstrated by various examples.

Cite As Get BibTex

Sarah Winkler. Extending Maximal Completion (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.3

Author Details

Sarah Winkler
  • University of Innsbruck, Austria

Funding

Supported by FWF (Austrian Science Fund) project T789.

Acknowledgements

The author is grateful to Deepak Kapur for his insightful comments.

References

  1. J. Avenhaus, T. Hillenbrand, and B. Löchner. On using ground joinable equations in equational theorem proving. J. Symb. Comput., 36(1-2):217-233, 2003. URL: http://dx.doi.org/10.1016/S0747-7171(03)00024-5.
  2. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: http://dx.doi.org/10.1017/CBO9781139172752.
  3. L. Bachmair. Canonical Equational Proofs. Progress in Theoretical Computer Science. Birkhäuser, 1991. Google Scholar
  4. L. Bachmair and N. Dershowitz. Completion for Rewriting Modulo a Congruence. Theor. Comput. Sci., 67(2,3):173-201, 1989. URL: http://dx.doi.org/10.1016/0304-3975(89)90003-0.
  5. L. Bachmair, N. Dershowitz, and Jieh Hsiang. Orderings for Equational Proofs. In Proc. 1st LICS, pages 346-357, 1986. Google Scholar
  6. L. Bachmair, N. Dershowitz, and D. A. Plaisted. Completion Without Failure. In H. Aït Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2 of Rewriting Techniques, pages 1-30. Academic Press, 1989. URL: http://dx.doi.org/10.1016/B978-0-12-046371-8.50007-9.
  7. N. Bjørner. Taking Satisfiability to the Next Level with Z3. In Proc. 6th IJCAR, volume 7364 of LNCS, pages 1-8, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31365-3_1.
  8. H. Devie. Linear Completion. In Proc. 2nd CTRS, pages 233-245. Springer, 1991. URL: http://dx.doi.org/10.1007/3-540-54317-1_94.
  9. V. D'Silva, L. Haller, and D. Kroening. Abstract Conflict Driven Learning. ACM SIGPLAN Notices, 48(1):143-154, 2013. URL: http://dx.doi.org/10.1145/2480359.2429087.
  10. B. Dutertre and L. de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In Proc. 18th CAV, volume 4144 of LNCS, pages 81-94, 2006. URL: http://dx.doi.org/10.1007/11817963_11.
  11. N. Hirokawa, A. Middeldorp, C. Sternagel, and S. Winkler. Infinite Runs in Abstract Completion. In Proc. 2nd FSCD, volume 84 of LIPIcs, pages 19:1-19:16, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.19.
  12. J.-P. Jouannaud and H. Kirchner. Completion of a Set of Rules Modulo a Set of Equations. SIAM Journal of Computation, 15(4):1155-1194, 1986. URL: http://dx.doi.org/10.1137/0215084.
  13. J.-P. Jouannaud and C. Marché. Termination and Completion Modulo Associativity, Commutativity and Identity. Theor. Comput. Sci., 104(1):29-51, 1992. URL: http://dx.doi.org/10.1016/0304-3975(92)90165-C.
  14. D. Kapur, D. R. Musser, and P. Narendran. Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure. J. Symb. Comput., 6(1):19-36, 1988. URL: http://dx.doi.org/10.1016/S0747-7171(88)80019-1.
  15. D. Kapur and H. Zhang. An overview of Rewrite Rule Laboratory (RRL). Comput. Math. Appl., 29(2):91-114, 1995. URL: http://dx.doi.org/10.1016/0898-1221(94)00218-A.
  16. D. Klein. Equational Reasoning and Completion. PhD thesis, Japan Advanced Institute of Science and Technology, 2012. Google Scholar
  17. D. Klein and N. Hirokawa. Maximal Completion. In Proc. 22nd RTA, volume 10 of LIPIcs, pages 71-80, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2011.71.
  18. D. E. Knuth and P. Bendix. Simple Word Problems in Universal Algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, 1970. URL: http://dx.doi.org/10.1016/B978-0-08-012975-4.
  19. L. Kovács and A. Voronkov. First-Order Theorem Proving and Vampire. In Proc. 25th CAV, volume 8044 of LNCS, pages 1-35, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39799-8_1.
  20. B. Löchner. A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. In Proc. 2nd IJCAR, volume 3097 of LNCS, pages 45-59, 2004. URL: http://dx.doi.org/10.1007/978-3-540-25984-8_2.
  21. C. Marché. Normalised Rewriting and Normalised Completion. In LICS 1994, pages 394-403. IEEE Computer Society, 1994. URL: http://dx.doi.org/10.1109/LICS.1994.316050.
  22. C. Marché. Normalized Rewriting: An Alternative to Rewriting Modulo a Set of Equations. J. Symb. Comput., 21(3):253-288, 1996. URL: http://dx.doi.org/10.1006/jsco.1996.0011.
  23. G. E. Peterson and M. E. Stickel. Complete Sets of Reductions for Some Equational Theories. J. ACM, 28(2):233-264, 1981. URL: http://dx.doi.org/10.1145/322248.322251.
  24. A. Rubio. A fully syntactic AC-RPO. Inform. Comput., 178(2):515-533, 2002. URL: http://dx.doi.org/10.1006/inco.2002.3158.
  25. H. Sato and S. Winkler. Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion. In Proc. 25th CADE, volume 9195 of LNCS, pages 152-162, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21401-6_10.
  26. A. Sattler-Klein. About changing the ordering during Knuth-Bendix completion. In Proc. 11th STACS, volume 775 of LNCS, pages 175-186, 1994. URL: http://dx.doi.org/10.1007/3-540-57785-8_140.
  27. P. Schultz and R. Wisnesky. Algebraic data integration. J. Funct. Program., 27(e24):51 pages, 2017. URL: http://dx.doi.org/10.1017/S0956796817000168.
  28. S. Schulz. System Description: E 1.8. In Proc. 19th LPAR, volume 8312 of LNCS, pages 735-743, 2013. URL: http://dx.doi.org/10.1007/978-3-642-45221-5_49.
  29. T. Sternagel and A. Middeldorp. Conditional Confluence (System Description). In Proc. RTA/TLCA 2014, volume 8560 of LNCS, pages 456-465, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08918-8_31.
  30. T. Sternagel, S. Winkler, and H. Zankl. Recording Completion for Certificates in Equational Reasoning. In Proc. 4th CPP, pages 41-47, 2015. URL: http://dx.doi.org/10.1145/2676724.2693171.
  31. G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts. J. Autom. Reasoning, 43(4):337-362, 2009. URL: http://dx.doi.org/10.1007/s10817-009-9143-8.
  32. I. Wehrman and A. Stump. Mining Propositional Simplification Proofs for Small Validating Clauses. Theor. Comput. Sci., 144(2):79-91, 2006. URL: http://dx.doi.org/10.1016/j.entcs.2005.12.008.
  33. S. Winkler. A Ground Joinability Criterion for Ordered Completion. In Proc. 6th IWC, pages 45-49, 2017. Google Scholar
  34. S. Winkler and A. Middeldorp. Normalized Completion Revisited. In Proc. 24th RTA, volume 21 of LIPIcs, pages 319-334, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2013319.
  35. S. Winkler and A. Middeldorp. Completion for Logically Constrained Rewriting. In Proc. 3rd FSCD, volume 108 of LIPIcs, pages 30:1-30:18, 2018. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2018.30.
  36. S. Winkler and G. Moser. MaedMax: A Maximal Ordered Completion Tool. In Proc. 9th IJCAR, volume 10900 of LNCS, pages 472-480, 2018. URL: http://dx.doi.org/10.1007/978-3-319-94205-6_31.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact