Left-linear completion with AC axioms. (English) Zbl 07838499
Pientka, Brigitte (ed.) et al., Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14132, 401-418 (2023).
Summary: We revisit AC completion for left-linear term rewrite systems where AC unification is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process. Finally, we present experimental results for our implementation of left-linear AC completion in the tool accompll.
For the entire collection see [Zbl 1535.68012].
For the entire collection see [Zbl 1535.68012].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Avenhaus, J., Reduktionssysteme (1995), Heidelberg: Springer, Heidelberg · Zbl 0827.68063 · doi:10.1007/978-3-642-79351-6 |
| [2] | Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998). doi:10.1017/CBO9781139172752 · Zbl 0948.68098 |
| [3] | Bachmair, L.: Canonical Equational Proofs. Progress in Theoretical Computer Science. Birkhäuser, Boston (1991). doi:10.1007/978-1-4684-7118-2 · Zbl 0732.68094 |
| [4] | Hirokawa, N., Middeldorp, A., Sternagel, C., Winkler, S.: Abstract completion, formalized. Logical Methods Comput. Sci. 15(3), 19:1-19:42 (2019). doi:10.23638/LMCS-15(3:19)2019 · Zbl 1509.68119 |
| [5] | Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 27, 4, 797-821 (1980) · Zbl 0458.68007 · doi:10.1145/322217.322230 |
| [6] | Jouannaud, JP; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 4, 1155-1194 (1986) · Zbl 0665.03005 · doi:10.1137/0215084 |
| [7] | Kapur, D.: A modular associative commutative (AC) congruence closure algorithm. In: Kobayashi, N. (ed.) Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics, vol. 195, pp. 15:1-15:21 (2021). doi:10.4230/LIPIcs.FSCD.2021.15 · Zbl 07700620 |
| [8] | Kapur, D.; Musser, DR; Narendran, P., Only prime superpositions need be considered in the Knuth-Bendix completion procedure, J. Symb. Comput., 6, 1, 19-36 (1988) · Zbl 0651.68029 · doi:10.1016/S0747-7171(88)80019-1 |
| [9] | Klein, D., Hirokawa, N.: Maximal completion. In: Schmidt-Schauß, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics, vol. 10, pp. 71-80 (2011). doi:10.4230/LIPIcs.RTA.2011.71 · Zbl 1236.68133 |
| [10] | 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 (1970). doi:10.1016/B978-0-08-012975-4.50028-X · Zbl 0188.04902 |
| [11] | Korp, M.; Sternagel, C.; Zankl, H.; Middeldorp, A.; Treinen, R., Tyrolean Termination Tool 2, Rewriting Techniques and Applications, 295-304 (2009), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-02348-4_21 |
| [12] | Marché, C., Normalized rewriting: an alternative to rewriting modulo a set of equations, J. Symb. Comput., 21, 3, 253-288 (1996) · Zbl 0859.68050 · doi:10.1006/jsco.1996.0011 |
| [13] | Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: Raamsdonk, F. (ed.) Proceedings of the 24th International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics, vol. 21, pp. 286-301 (2013). doi:10.4230/LIPIcs.RTA.2013.287 · Zbl 1356.68201 |
| [14] | Sternagel, T.; Zankl, H.; Gramlich, B.; Miller, D.; Sattler, U., KBCV - Knuth-Bendix completion visualizer, Automated Reasoning, 530-536 (2012), Heidelberg: Springer, Heidelberg · Zbl 1358.68160 · doi:10.1007/978-3-642-31365-3_41 |
| [15] | Wehrman, I.; Stump, A.; Westbrook, E.; Pfenning, F., Slothrop: Knuth-Bendix completion with a modern termination checker, Term Rewriting and Applications, 287-296 (2006), Heidelberg: Springer, Heidelberg · Zbl 1151.68456 · doi:10.1007/11805618_22 |
| [16] | Winkler, S.: Termination tools in automated reasoning. Ph.D. thesis, University of Innsbruck (2013) |
| [17] | Winkler, S.: Extending maximal completion. In: Geuvers, H. (ed.) Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics, vol. 131, pp. 3:1-3:15 (2019). doi:10.4230/LIPIcs.FSCD.2019.3 · Zbl 1528.68168 |
| [18] | Winkler, S.; Middeldorp, A.; Bjørner, N.; Sofronie-Stokkermans, V., AC completion with termination tools, Automated Deduction - CADE-23, 492-498 (2011), Heidelberg: Springer, Heidelberg · Zbl 1341.68198 · doi:10.1007/978-3-642-22438-6_37 |
| [19] | Winkler, S., Middeldorp, A.: Normalized completion revisited. In: Raamsdonk, F. (ed.) Proceedings of the 24th International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics, vol. 21, pp. 318-333 (2013). doi:10.4230/LIPIcs.RTA.2013.319 · Zbl 1356.68127 |
| [20] | Winkler, S.; Sato, H.; Middeldorp, A.; Kurihara, M., Multi-completion with termination tools, J. Autom. Reason., 50, 3, 317-354 (2013) · Zbl 1362.68253 · doi:10.1007/s10817-012-9249-2 |
| [21] | Yamada, A.; Kusakari, K.; Sakabe, T.; Dowek, G., Nagoya Termination Tool, Rewriting and Typed Lambda Calculi, 466-475 (2014), Cham: Springer, Cham · Zbl 1416.68183 · doi:10.1007/978-3-319-08918-8_32 |
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.
