×

AC-KBO revisited. (English) Zbl 1379.68277

Summary: Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this paper, we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful version, and we modify the latter to amend its lack of monotonicity on non-ground terms. We further present new complexity results. An extension reflecting the recent proposal of subterm coefficients in standard Knuth-Bendix orders is also given. The various orders are compared on problems in termination and completion.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
06A06 Partial orders, general
68Q42 Grammars and rewriting systems

Software:

REVE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] AlarcónB., LucasS. and MeseguerJ.2010. A dependency pair framework for A ∨ C-termination. In Proc. 8th International Workshop on Rewriting Logic and its Applications (WRLA 2010), Lecture Notes in Computer Science, vol. 6381. Springer Berlin Heidelberg, 35-51. · Zbl 1306.68060
[2] ArtsT. and GieslJ.2000. Termination of term rewriting using dependency pairs. Theoretical Computer Science236, 1-2, 133-178.10.1016/S0304-3975(99)00204-2 · Zbl 0940.00059 · doi:10.1016/S0304-3975(99)00204-2
[3] BachmairL. and PlaistedD. A.1985. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation1, 329-349.10.1016/S0747-7171(85)80019-5 · Zbl 0587.68041 · doi:10.1016/S0747-7171(85)80019-5
[4] BenCherifa, A and LescanneP.1987. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming9, 2, 137-159.10.1016/0167-6423(87)90030-X · Zbl 0625.68036 · doi:10.1016/0167-6423(87)90030-X
[5] CodishM., GieslJ., Schneider-KampP. and ThiemannR.2012. SAT solving for termination proofs with recursive path orders and dependency pairs. Journal of Automated Reasoning49, 1, 53-93.10.1007/s10817-010-9211-0 · Zbl 1276.68140 · doi:10.1007/s10817-010-9211-0
[6] DershowitzN.1982. Orderings for term-rewriting systems. Theoretical Computer Science17, 3, 279-301.10.1016/0304-3975(82)90026-3 · Zbl 0525.68054 · doi:10.1016/0304-3975(82)90026-3
[7] GieslJ. and KapurD.2001. Dependency pairs for equational rewriting. In Proc. 12th International Conference on Rewriting Techniques and Applications (RTA 2001), Lecture Notes in Computer Science, vol. 2051. Springer Berlin Heidelberg, 93-108. · Zbl 0981.68063
[8] KnuthD. and BendixP.1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, J.Leech, Ed. Pergamon Press, New York, 263-297.
[9] KorovinK. and VoronkovA.2003a. An AC-compatible Knuth-Bendix order. In Proc. 19th International Conference on Automated Deduction (CADE 2003), Lecture Notes in Artificial Intelligence, vol. 2741. Springer Berlin Heidelberg, 47-59. · Zbl 1278.68268
[10] KorovinK. and VoronkovA.2003b. Orienting rewrite rules with the Knuth-Bendix order. Information and Computation183, 2, 165-186.10.1016/S0890-5401(03)00021-X · Zbl 1054.68079 · doi:10.1016/S0890-5401(03)00021-X
[11] KrishnamoorthyM. and NarendranP.1985. On recursive path ordering. Theoretical Computer Science40, 323-328.10.1016/0304-3975(85)90175-6 · Zbl 0602.68031 · doi:10.1016/0304-3975(85)90175-6
[12] KusakariK.2000. AC-termination and dependency pairs of term rewriting systems. Ph.D. thesis, JAIST, Nomi, Japan.
[13] KusakariK. and ToyamaY.2001. On proving AC-termination by AC-dependency pairs. IEICE Transactions on Information and SystemsE84-D, 5, 439-447.
[14] LankfordD.1979. On proving term rewrite systems are noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA.
[15] LöchnerB.2006. Things to know when implementing KBO. Journal of Automated Reasoning36, 4, 289-310. · Zbl 1107.68098
[16] LudwigM. and WaldmannU.2007. An extension of the Knuth-Bendix ordering with LPO-like properties. In Proc. 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2007), Lecture Notes in Artificial Intelligence, vol. 4790. Springer Berlin Heidelberg, 348-362. · Zbl 1137.03306
[17] MarchéC. and UrbainX.2004. Modular and incremental proofs of AC-termination. Journal of Symbolic Computation38, 1, 873-897.10.1016/j.jsc.2004.02.003 · Zbl 1137.68419 · doi:10.1016/j.jsc.2004.02.003
[18] MiddeldorpA. and ZantemaH.1997. Simple termination of rewrite systems. Theoretical Computer Science175, 1, 127-158.10.1016/S0304-3975(96)00172-7 · Zbl 0903.68106 · doi:10.1016/S0304-3975(96)00172-7
[19] RubioA.2002. A fully syntactic AC-RPO. Information and Computation178, 2, 515-533.10.1006/inco.2002.3158 · Zbl 1049.68076 · doi:10.1006/inco.2002.3158
[20] SchrijverA.1986. Theory of Linear and Integer Programming. Wiley, West Sussex, England. · Zbl 0665.90063
[21] SteinbachJ.1990. AC-termination of rewrite systems: A modified Knuth-Bendix ordering. In Proc. 2nd International Conference on Algebraic and Logic Programming (ALP 1990), Lecture Notes in Computer Science, vol. 463. Springer Berlin Heidelberg, 372-386. · Zbl 1493.68179
[22] ThiemannR., AllaisG. and NageleJ.2012. On the formalization of termination techniques based on multiset orderings. In Proc. 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Leibniz International Proceedings in Informatics, vol. 15. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 339-354.
[23] WinklerS.2013. Termination tools in automated reasoning. Ph.D. thesis, UIBK, Innsbruck, Austria.
[24] WinklerS., ZanklH. and MiddeldorpA.2012. Ordinals and Knuth-Bendix orders. In Proc. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), LNCS Advanced Research in Computing and Software Science, vol. 7180. Springer Berlin Heidelberg, 420-434.
[25] YamadaA., WinklerS., HirokawaN. and MiddeldorpA.2014. AC-KBO revisited. In Proc. 12th International Symposium on Functional and Logic Programming (FLOPS 2014), Lecture Notes in Computer Science, vol. 8475. Springer International Publishing, 319-335.
[26] ZanklH., HirokawaN. and MiddeldorpA.2009. KBO orientability. Journal of Automated Reasoning43, 2, 173-201.10.1007/s10817-009-9131-z · Zbl 1184.68303 · doi:10.1007/s10817-009-9131-z
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.