maedmax: Maximal Ordered Completion

General

maedmax is a tool for (ordered) completion and equational theorem proving.
It is based on maximal ordered completion. This new approach extends the maxSMT-based method for standard completion developed by Klein and Hirokawa (2011) to ordered completion and theorem proving. M├ŽdMax focuses on satisfiability, incorporating powerful ground completeness checks. Proofs can be output in a format that is certifiable by the Isabelle-based certifier CeTA. It also provides an order generation mode which can be used to synthesize term orderings for other tools.

A system description submitted to IJCAR 2018 can be found here.

Usage

The tool can be used via its web interface or as a command line tool. In the latter case, with default options (as used in the experiments) maedmax is simply invoked by providing an input file, for example:
$ ./maedmax examples/RNG042-2.tptp
The input file may be in TPTP or trs format. Here are an example TPTP and an example trs input.

Download

You may want to download a binary for 64-bit Linux, or the sources from github.

Experiments

Comparison of maedmax with other tools on different data sets:
Experiments evaluating particular features of maedmax:
Experiments evaluating order generation mode on E:
Examples


Options

maedmax allows for a variety of options, in case you want to control the search strategy or obtain a particular output format. Example calls include the following:

In case you want to dive into the gory details, please find here an explanation of all available options.