Chapter 5 Lab: First-Order Logic

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

@dataclass
class Variable:
    name: str
    
    def __str__(self):
        return self.name

@dataclass
class Constant:
    name: str
    
    def __str__(self):
        return self.name

@dataclass
class Function:
    name: str
    args: List['Term']
    
    def __str__(self):
        args_str = ', '.join(str(arg) for arg in self.args)
        return f"{self.name}({args_str})"

Term = Union[Variable, Constant, Function]

@dataclass
class Predicate:
    name: str
    args: List[Term]
    
    def __str__(self):
        args_str = ', '.join(str(arg) for arg in self.args)
        return f"{self.name}({args_str})"

def substitute(term: Term, subst: Dict[str, Term]) -> Term:
    """
    TODO: Apply substitution to term
    Replace variables according to substitution dictionary
    """
    pass

def occurs_check(var: Variable, term: Term) -> bool:
    """
    TODO: Check if variable occurs in term
    Prevents infinite structures like X = f(X)
    """
    pass

# Test
X = Variable('X')
Y = Variable('Y')
a = Constant('a')
b = Constant('b')
f = Function('f', [X, a])

subst = {'X': b, 'Y': f}
print(f'Term: {f}')
print(f'After substitution: {substitute(f, subst)}')
print(f'Occurs check X in f(X, a): {occurs_check(X, f)}')

def unify(term1: Term, term2: Term, subst: Dict[str, Term] = None) -> Optional[Dict[str, Term]]:
    """
    TODO: Implement unification algorithm
    
    Algorithm:
    1. If terms are identical, return current substitution
    2. If term1 is variable:
       - If already bound, unify with binding
       - Otherwise, add binding if occurs check passes
    3. If term2 is variable: symmetric case
    4. If both are functions:
       - Names must match
       - Recursively unify arguments
    5. Otherwise: fail (return None)
    
    Return: Substitution dict or None if unification fails
    """
    pass

def unify_predicates(pred1: Predicate, pred2: Predicate) -> Optional[Dict[str, Term]]:
    """Unify two predicates"""
    if pred1.name != pred2.name or len(pred1.args) != len(pred2.args):
        return None
    
    subst = {}
    for arg1, arg2 in zip(pred1.args, pred2.args):
        subst = unify(arg1, arg2, subst)
        if subst is None:
            return None
    return subst

# Test cases
test_cases = [
    (Variable('X'), Constant('a')),
    (Variable('X'), Variable('Y')),
    (Function('f', [Variable('X')]), Function('f', [Constant('a')])),
    (Function('f', [Variable('X'), Variable('X')]), Function('f', [Constant('a'), Constant('b')])),  # Should fail
]

for t1, t2 in test_cases:
    result = unify(t1, t2)
    print(f'unify({t1}, {t2}) = {result}')

class FOLKnowledgeBase:
    def __init__(self):
        self.facts = []  # Ground facts
        self.rules = []  # Horn clauses
        
    def add_fact(self, predicate: Predicate):
        self.facts.append(predicate)
        
    def add_rule(self, premises: List[Predicate], conclusion: Predicate):
        self.rules.append((premises, conclusion))
        
    def query(self, goal: Predicate) -> List[Dict[str, Term]]:
        """
        TODO: Find all substitutions that satisfy goal
        Use backward chaining
        """
        pass

# Build family tree KB
kb = FOLKnowledgeBase()

# Facts: Parent relationships
kb.add_fact(Predicate('Parent', [Constant('John'), Constant('Mary')]))
kb.add_fact(Predicate('Parent', [Constant('John'), Constant('Bob')]))
kb.add_fact(Predicate('Parent', [Constant('Mary'), Constant('Ann')]))

# Rules
# Grandparent(X, Z) :- Parent(X, Y), Parent(Y, Z)
X, Y, Z = Variable('X'), Variable('Y'), Variable('Z')
kb.add_rule(
    [Predicate('Parent', [X, Y]), Predicate('Parent', [Y, Z])],
    Predicate('Grandparent', [X, Z])
)

# Sibling(X, Y) :- Parent(Z, X), Parent(Z, Y), X != Y
kb.add_rule(
    [Predicate('Parent', [Z, X]), Predicate('Parent', [Z, Y])],
    Predicate('Sibling', [X, Y])
)

# Test queries
print('Query: Grandparent(John, X)?')
results = kb.query(Predicate('Grandparent', [Constant('John'), Variable('X')]))
for r in results:
    print(f'  X = {r.get("X")}')

def forward_chaining_fol(kb: FOLKnowledgeBase, max_iterations=100) -> Set[Predicate]:
    """
    TODO: Implement forward chaining for FOL
    
    Algorithm:
    1. Start with known facts
    2. For each rule:
       - Try to unify rule premises with known facts
       - If successful, instantiate conclusion and add as new fact
    3. Repeat until no new facts or max iterations
    
    Return: Set of all derived facts
    """
    pass

def match_premises(premises: List[Predicate], facts: List[Predicate]) -> List[Dict[str, Term]]:
    """
    TODO: Find all ways to match rule premises with facts
    Return list of substitutions
    """
    pass

# Test with transitivity
kb = FOLKnowledgeBase()

# Facts
kb.add_fact(Predicate('Edge', [Constant('a'), Constant('b')]))
kb.add_fact(Predicate('Edge', [Constant('b'), Constant('c')]))
kb.add_fact(Predicate('Edge', [Constant('c'), Constant('d')]))

# Rule: Path(X, Z) :- Edge(X, Y), Path(Y, Z)
# Rule: Path(X, Y) :- Edge(X, Y)
X, Y, Z = Variable('X'), Variable('Y'), Variable('Z')
kb.add_rule([Predicate('Edge', [X, Y])], Predicate('Path', [X, Y]))
kb.add_rule(
    [Predicate('Edge', [X, Y]), Predicate('Path', [Y, Z])],
    Predicate('Path', [X, Z])
)

derived = forward_chaining_fol(kb)
print('Derived facts:')
for fact in derived:
    print(f'  {fact}')

class PrologInterpreter:
    """Mini Prolog interpreter"""
    
    def __init__(self):
        self.kb = FOLKnowledgeBase()
        
    def parse_term(self, s: str) -> Term:
        """Parse string to term"""
        # YOUR CODE: Simple parser
        pass
        
    def parse_predicate(self, s: str) -> Predicate:
        """Parse string to predicate"""
        # YOUR CODE
        pass
        
    def backward_chain(self, goal: Predicate, depth=0, max_depth=10) -> List[Dict[str, Term]]:
        """
        TODO: Implement backward chaining with depth limit
        
        Algorithm:
        1. Try to unify goal with facts
        2. Try to unify goal with rule conclusions
        3. Recursively prove rule premises
        4. Collect all successful substitutions
        """
        pass
        
    def query(self, query_str: str) -> List[Dict[str, Term]]:
        """Execute query and return results"""
        goal = self.parse_predicate(query_str)
        return self.backward_chain(goal)

# Example: List operations
interpreter = PrologInterpreter()

# Define list predicates
# member(X, [X|_]).
# member(X, [_|T]) :- member(X, T).

# append([], L, L).
# append([H|T1], L2, [H|T3]) :- append(T1, L2, T3).

# Test
print("Query: member(2, [1,2,3])?")
# results = interpreter.query("member(2, [1,2,3])")
# print(results)

def skolemize(formula):
    """
    CHALLENGE: Convert formula to Skolem normal form
    
    1. Eliminate existential quantifiers by replacing with Skolem functions
    2. Move universal quantifiers to front
    3. Convert to CNF
    """
    pass

def resolution_fol(clauses: List[List[Predicate]]) -> bool:
    """
    CHALLENGE: FOL resolution
    Similar to propositional but with unification
    """
    pass