Description
The tool accompll performs AC completion for left-linear term rewrite systems and is written in Haskell. The used completion technique does not have to deal with AC unification but only works if the resulting system is left-linear.
News
Source code
Together with more detailed information, the source code is available at GitHub.Experiments
- completion with TTT2 and muterm vs mkbTT and MaedMax (LMCS 2024)
- completion with TTT2 vs mkbTT and MaedMax (CADE 2023)
Publications
-
J. Niederhauser and N. Hirokawa and A. Middeldorp
Left-Linear Completion with AC Axioms (extended version)
Proceedings of the 29th International Conference on Automated Deduction (CADE 2023)
LNAI 14132, pp. 401 – 418, 2023
-
J. Niederhauser and N. Hirokawa and A. Middeldorp
Church-Rosser Modulo for Left-Linear TRSs Revisited
Proceedings of the 12th International Workshop on Confluence (IWC 2023)
pp. 14 – 19, 2023