MELIA is a theorem prover for the Model Evolution Calculus with Equality and built-in linear integer arithmetic.

MELIA accepts formulas in the TPTP FOF, TFF, and TFF-INT formats (see the TPTP technical report). It includes a pre-processor for transforming such formulas into (sorted) constrained clauses, as prescribed by the calculus. MELIA features a variety of flag settings to control its search, e.g., for selecting literals to focus inferences on.

MELIA has been written from scratch in Scala and runs on the Java virtual machine. It is in a very early stage of development and has not been tuned for performance. When integer arithmetic is involved, MELIA is incomplete even if theoretically unneccessary. These issues will be addressed in forthcoming releases.

Relevant papers

See here for full bibliographic details.


Author: Peter Baumgartner, NICTA