This repo contains a series of Maude scripts for generating and checking proof certificates for syntactic unification and anti-unification in (Applicative) Matching Logic.

Prerequisites: Python 3, Maude, and Git.

Step 1: Open a terminal, cd into your working dir and type:

-$ git clone https://github.com/andreiarusoaie/certifying-unification-in-aml.git
-$ cd certifying-unification-in-aml

Step 2: Create an input file. Here is an example from our test suite:

-$  cat tests/samples/13_paper_cons_succ.in
variables: x1, x2, l1, l2
symbols: cons, succ, zero
problem: cons(succ(x1), cons(zero, l1)) =? cons(x2, cons(succ(x2), l2))

The variables and symbols sections describe the syntax of the input terms. problem is the (anti)unification problem to be solved.

Step 3: Generate the certificate (anti-unification):

-$ python3 ml-antiunify.py tests/samples/13_paper_cons_succ.in
...

This will generate the proof and it will also check whether the proof is correct (i.e., certification). The output for this particular call is available here.

Note: The certificates for unification can be generated by calling the ml-unify.py script on the same input:

-$ python3 ml-unify.py tests/samples/13_paper_cons_succ.in

You can contact me at andrei . arusoaie at uaic ro.