Skip to article frontmatterSkip to article content
Site not loading correctly?

This may be due to an incorrect BASE_URL configuration. See the MyST Documentation for reference.

Chapter 4: Propositional Logic - Implementation

from typing import List, Set, Dict, Tuple, Optional
from dataclasses import dataclass
from abc import ABC, abstractmethod

print('Libraries imported')
class Expr(ABC):
    @abstractmethod
    def evaluate(self, model: Dict[str, bool]) -> bool:
        pass
    
    @abstractmethod
    def get_symbols(self) -> Set[str]:
        pass

class Symbol(Expr):
    def __init__(self, name: str):
        self.name = name
    def evaluate(self, model):
        return model.get(self.name, False)
    def get_symbols(self):
        return {self.name}
    def __str__(self):
        return self.name

class Not(Expr):
    def __init__(self, operand):
        self.operand = operand
    def evaluate(self, model):
        return not self.operand.evaluate(model)
    def get_symbols(self):
        return self.operand.get_symbols()
    def __str__(self):
        return f'~{self.operand}'

class And(Expr):
    def __init__(self, *operands):
        self.operands = list(operands)
    def evaluate(self, model):
        return all(op.evaluate(model) for op in self.operands)
    def get_symbols(self):
        return set().union(*(op.get_symbols() for op in self.operands))
    def __str__(self):
        return '(' + ' & '.join(str(op) for op in self.operands) + ')'

class Or(Expr):
    def __init__(self, *operands):
        self.operands = list(operands)
    def evaluate(self, model):
        return any(op.evaluate(model) for op in self.operands)
    def get_symbols(self):
        return set().union(*(op.get_symbols() for op in self.operands))
    def __str__(self):
        return '(' + ' | '.join(str(op) for op in self.operands) + ')'

class Implies(Expr):
    def __init__(self, ant, cons):
        self.antecedent = ant
        self.consequent = cons
    def evaluate(self, model):
        return not self.antecedent.evaluate(model) or self.consequent.evaluate(model)
    def get_symbols(self):
        return self.antecedent.get_symbols() | self.consequent.get_symbols()
    def __str__(self):
        return f'({self.antecedent} -> {self.consequent})'

print('Expression classes defined')
def truth_table(expr, show=True):
    symbols = sorted(expr.get_symbols())
    n = len(symbols)
    
    if show:
        print(' | '.join(symbols) + ' | ' + str(expr))
        print('-' * 50)
    
    for i in range(2**n):
        model = {}
        row = []
        for j, sym in enumerate(symbols):
            val = bool((i >> (n-j-1)) & 1)
            model[sym] = val
            row.append('T' if val else 'F')
        result = expr.evaluate(model)
        row.append('T' if result else 'F')
        if show:
            print(' | '.join(row))

print('Truth table function defined')
print('=== Example: Implication ===')
P = Symbol('P')
Q = Symbol('Q')
impl = Implies(P, Q)
truth_table(impl)
class KnowledgeBase:
    def __init__(self):
        self.facts = set()
        self.rules = []
    
    def tell_fact(self, fact):
        self.facts.add(fact)
    
    def tell_rule(self, premises, conclusion):
        self.rules.append((premises, conclusion))
    
    def forward_chain(self, query, verbose=True):
        inferred = set(self.facts)
        agenda = list(self.facts)
        
        while agenda:
            fact = agenda.pop(0)
            if fact == query:
                if verbose: print(f'Proved: {query}')
                return True
            
            for premises, conclusion in self.rules:
                if conclusion not in inferred and all(p in inferred for p in premises):
                    inferred.add(conclusion)
                    agenda.append(conclusion)
                    if verbose: print(f'Inferred: {conclusion}')
        return False

print('KnowledgeBase implemented')
print('=== Example: Animal Classification ===')
kb = KnowledgeBase()
kb.tell_fact('hasFur')
kb.tell_fact('produceMilk')
kb.tell_rule(['hasFur', 'produceMilk'], 'mammal')
kb.tell_rule(['mammal', 'eatsMeat'], 'carnivore')

print('Query: mammal')
kb.forward_chain('mammal')

Real-World: Sudoku Solver

Encoding Sudoku as propositional logic SAT problem.