Programming Lab 3: First-Order Unification

Submission deadline: Wednesday, July 6, 2016 (11:59 p.m.)

TA: Diego Alejandro Montoya-Zapata

Introduction

The aim of this programming assignment is to implement unification in first-order logic (FOL). Unification is one of the main steps to perform resolution in FOL.

A substitution of terms for variables is a set

        {x₁ ← t₁, ..., x_n ← t_n}

where each x_i is a distinct variable and each t_i is a term which is not identical to the corresponding variable x_i. The empty substution is the empty set [Ben-Ari (2012), Definition 10.4].

Let U = {A₁, ..., A_n} be a set of atoms. A unifier θ is a substitution such that:

        A₁θ = ... = A_nθ.

A most general unifier (MGU) for U is a unifier μ such that any unifier θ of U can be expressed as:

        θ = μλ

for some substitution λ [Ben-Ari (2012), Definition 10.11].

Assignment (80%)

(35%) Write a Haskell or Prolog program which finds the MGU (if exists) of two atoms in FOL. In case the MGU does not exists, the program must report it.
- Haskell: The module FOL defines a data type for the atoms in FOL. This module can be found in the GitHub repository logic-cm0845- lab3.
  Using the module FOL, define a function
```
            unify :: Atom -> Atom -> [Atom]
          
```
  that returns a list with the atoms obtained after performing the substitution expressed by the MGU of the two given atoms in FOL.
- Prolog: write a Prolog predicate unify(A1,A2,B) where B is a list with the atoms obtained after performing the substitution expressed by the MGU of A1 and A2.
(35%) Oral exposition. Answers and explanations given in the revision of the lab.
(10%) Annotate your source code in a way that explains your solution for the assignment.

Clean code (10%)

Before submitting your code, clean it up! Clean code:

Does not have long lines (at most 80 columns).
Has a consistent layout.
Has type signatures for everything.
Has good comments.
Has no junk (unused code, commented code, unnecessary code).
Has no overly complicated function definitions.
Does not contain any repetitive code.
Has no unnecessary spaces at the end of a line, or empty lines at the end of a file (see: Fixing trailing whitespace issues with Emacs).

Submission (10%)

Submission is electronic. Send an email to asr(at)eafit(dot)edu(dot)co and dmonto39(at)eafit(dot)edu(dot)co and attach a compressed file (.zip or .tar.gz) with your solution.

Your submission has to include the following:

Unification.hs or unification.pl, a file with your solution for the assignment.
README.txt (or README.md), a file containing at least the following information:
- The name of your program.
- Your name.
- A general description of your program.
- Information on how to use your program.
- A detailed description of the output format of your program.

Notes

The programming lab is individual.
In case you decide to use Haskell:
- You are to use the Haskell Platform ≥ 7.10.2-a or GHC ≥ 7.10.2.
- You can add class constraints to the type signature of your functions if you need them.

Bibliography

Ben-Ari, Mordechai (2012). Mathematical Logic for Computer Science. 3rd ed. Springer.

CM0845 Logic