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 the sources from github or the following binaries (64-bit):

• maedmax 1.4 including WPO (September 19)
• maedmax 1.3 (February 2019)

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/GRP154-1.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/RNG042-2.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 RNG042-2.p
  Possible values for -M are olpo for LPO, okbo for KBO, or olpokbo 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).
• 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.