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
Additional information can be found here.
You can contact me at andrei . arusoaie at uaic ro.