General
maedmax is a tool for (ordered) completion and equational theorem proving.It is based on maximal ordered completion. This new approach extends the maxSMTbased 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 Isabellebased 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/RNG0422.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 64bit Linux, or the sources from github.Experiments
Comparison of maedmax with other tools on different data sets: results on TPTP 6.4.0 UEQ SAT (600s timeout)
 results on TPTP 6.4.0 UEQ UNSAT, including verified CPF proofs (600s timeout)
 results on 731 ConCon examples (60s timeout)
 results on 23 Examples from the paper Ordered Rewriting and Confluence by U. Martin and T. Nipkow
 results on 139 completion examples from the paper Encoding DP Techniques and Control Strategies for Maximal Completion by H. Sato and S. Winkler (60s timeout)
 certified CPF proofs for TPTP 6.4.0 UEQ UNSAT
Experiments evaluating particular features of maedmax:
 without vs with fingerprint indexing (timeout 60s)
 pure LPO and KBO vs mixed strategy employing restarts (timeout 60s)
Experiments evaluating order generation mode on E:
 TPTP UEQ SAT (timeout 60s)
 TPTP UEQ UNSAT (timeout 60s)
Examples
 amphibians_100, amphibians_200 examples generated by the AQL tool
 Boolean ring example (Example 1 from the paper)
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 order to obtain a certifiable proof output, you can call
./maedmax cpf examples/GRP1541.tptp
 In order to consider ground joinability over an extended signature (please cf. the paper for
details) you can call
$ ./maedmax xsig examples/MN90_Ex4_5_ACgroups_exp2.tptp
 In order to use a timeout of 5 seconds, apply only LPO as termination strategy, select
2 TRSs per iteration and allow 10 new equations per TRS, you would call
$ ./maedmax T 5 M olpo K 2 N 10 examples/RNG0422.tptp
In case you want to dive into the gory details, please find here an explanation of all available options.
 A timeout in seconds can be specified using option
T
.  The termination strategy can be controlled with the option
M
, which takes an additional string specifying the strategy. An example call is
$ ./maedmax M olpo RNG0422.p
Possible values forM
areolpo
for LPO,okbo
for KBO, orolpokbo
for a combination (which is the default).  Ground joinability is attempted to be proven over an extended signature, i.e., the
signature extended by infinitely many constants, when using option
xsig
.  The tool attempts to produce a proof in the certifiable CPF format when called
with option
cpf
.  The tool can also be run in standard completion mode using option
kb
. In this mode it closely resembles maxcomp.  A number of options allows to control parameters of the maximal completion procedure
and the ground confluence checks. All of the following require to specify a natural number.

Option
K
controls the number of TRSs selected in every iteration. 
Option
N
controls how many passive equations are added to the set of active facts, per selected TRS.  The instantiation depth of ground joinability checks is controlled by
I
(cf. the number of repetitions in the strategy given on p.9 of the paper).

Option
 The remaining options are mainly there for analyzing input problems and debugging.

Option
term
performs a termination check of the input system, considering the rules to be oriented as given. 
Option
analyze
prints problem properties, including recognized theories.  Debugging output is triggered by the option
D
.

Option