- Maxcomp is a fully automatic completion tool for equational systems.
- Moca is a fully automatic first-order theorem prover for Horn clauses.
Source Code for Linux
Moca v0.1 released. This version participates in
the 9th Confluence Competition (CoCo 2019).
(April 10, 2019; first release)
- Maxcomp v1.1
(March 9, 2015; support for ocamlyices 0.7.1)
- Dominik Klein and Nao Hirokawa.
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
- Nao Hirokawa
- Dominik Klein
- Yusuke Oi