Chapter 5: First-Order Logic - Implementation - Artificial Intelligence

from typing import Dict, List, Optional
from dataclasses import dataclass

print('Imports complete')

@dataclass
class Term:
    name: str
    is_variable: bool

@dataclass
class Predicate:
    name: str
    args: List[Term]

def unify(p1: Term, p2: Term, subst: Dict = None) -> Optional[Dict]:
    if subst is None:
        subst = {}
    
    if p1.name == p2.name:
        return subst
    elif p1.is_variable:
        subst[p1.name] = p2
        return subst
    elif p2.is_variable:
        subst[p2.name] = p1
        return subst
    else:
        return None

print('Unification implemented')

print('=== Unification Example ===')
x = Term('x', True)
john = Term('John', False)
result = unify(x, john)
print(f'Unify(x, John) = {result}')

Next Steps: Family Relations¶

The lab notebook (Chapter 5 Lab: First-Order Logic) builds a family knowledge base with Parent facts and rules such as

Grandparent(X, Z) :- Parent(X, Y), Parent(Y, Z)
Sibling(X, Y)     :- Parent(Z, X), Parent(Z, Y), X ≠ Y

With Parent(John, Mary), Parent(John, Bob) and Parent(Mary, Ann), forward chaining should derive Grandparent(John, Ann), Sibling(Mary, Bob) and Sibling(Bob, Mary). Leaving out the X ≠ Y test also derives Sibling(Mary, Mary): a good check that your implementation enforces it.