Chapter 5: First-Order Logic - Implementation

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}')