Maxcomp and Toma

About

Maxcomp is a fully automatic completion tool for equational systems.
Toma is a fully automatic first-order equational theorem prover. (Previously it was called Tofu.)
Moca is a fully automatic first-order theorem prover for Horn clauses.

Toma v0.6
(January 24, 2024: Adopted MIT license.)
Maxcomp v1.5
(June 26, 2021: Improved performance on (E)LPO.)
Moca v0.3
(July 1, 2024: Supported CPF 3; Adopted MIT license. This version participates in CoCo 2024.)

Maxcomp v1.4
(June 7, 2021: Improved performance on rewriting.)
Maxcomp v1.3
(May 27, 2021: Fixed a bug related to EKBO.)
Maxcomp v1.2
(May 8, 2021: Supports ELPO, EKBO, and inter-reduction.)
Maxcomp v1.1
(August 5, 2019: Support for ocamlyices 0.7.1)
Maxcomp v1.0
(March 9, 2015: Released.)

Toma v0.5
(July 31, 2023: Restored the infeasibility mode for CoCo.) Toma v0.4
(June 19, 2023: Released. This version participates in CASC-29.)
Toma v0.3
(February 17, 2023: Supported generalized weighted path orders.)
Toma v0.2
(July 19, 2022: Released. This version participates in CASC-J11.)
Tofu v0.1
(May 15, 2022: Released.)

Moca v0.2
(Dec 22, 2020: Improved encodings for Horn clauses.)
Moca v0.1 released. This version participates in the infeasibility category (INF) of CoCo 2019.

Saito Teppei and Nao Hirokawa.
Weighted Path Orders are Semantic Path Orders
Proceedings of the 14th International Symposium on Frontiers of Combining Systems, LNCS/LNAI, 2023.
problem set and experimental data
Nao Hirokawa.
Completion and Reduction Orders
Proceedings of the 5th International Conference on Formal Structures on Computation and Deduction, Leibniz International Proceedings in Informatics 195, pp. 2:1–2:9, 2021.
problem set and experimental data
Dominik Klein and Nao Hirokawa.
Maximal Completion
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics 10, pp. 71-80, 2011.
problem set; experimental data