Knowledge Representation & Reasoning

"""
AI Track Unit 5: Knowledge Representation & Logical Inference Engine
Forward Chaining, Backward Chaining, and Resolution Refutation
Author: DevAscent Engineering Team
"""

from typing import List, Set, Dict, Optional, Tuple

# =====================================================================
# 1. HORN CLAUSE KNOWLEDGE BASE & CHAINING ENGINES
# =====================================================================
class HornClause:
    def __init__(self, premises: List[str], conclusion: str):
        self.premises: List[str] = premises
        self.conclusion: str = conclusion

    def __repr__(self):
        if not self.premises:
            return f"Fact({self.conclusion})"
        return f"{' ^ '.join(self.premises)} -> {self.conclusion}"

class KnowledgeBase:
    def __init__(self):
        self.clauses: List[HornClause] = []
        self.facts: Set[str] = set()

    def tell_fact(self, fact: str):
        self.facts.add(fact)

    def tell_rule(self, premises: List[str], conclusion: str):
        self.clauses.append(HornClause(premises, conclusion))

    # -----------------------------------------------------------------
    # Forward Chaining Algorithm
    # -----------------------------------------------------------------
    def forward_chain(self, query: str) -> Tuple[bool, List[str]]:
        """
        Data-driven bottom-up inference.
        Returns (is_entailed, derivation_order).
        """
        known_facts = set(self.facts)
        if query in known_facts:
            return True, [query]

        # Count of unsatisfied premises for each clause
        count = {clause: len(clause.premises) for clause in self.clauses}
        agenda = list(self.facts)
        derivation_order = []

        while agenda:
            p = agenda.pop(0)
            derivation_order.append(p)

            for clause in self.clauses:
                if p in clause.premises:
                    count[clause] -= 1
                    # If all premises satisfied, fire rule
                    if count[clause] == 0:
                        concl = clause.conclusion
                        if concl == query:
                            derivation_order.append(concl)
                            return True, derivation_order
                        if concl not in known_facts:
                            known_facts.add(concl)
                            agenda.append(concl)

        return False, derivation_order

    # -----------------------------------------------------------------
    # Backward Chaining Algorithm
    # -----------------------------------------------------------------
    def backward_chain(self, query: str, visited: Optional[Set[str]] = None) -> bool:
        """
        Goal-driven top-down recursive inference.
        """
        if visited is None:
            visited = set()

        # If already known as base fact, base case succeeded
        if query in self.facts:
            return True

        if query in visited:
            return False  # Prevent infinite loops in circular rules
        visited.add(query)

        # Find all rules concluding this query
        for clause in self.clauses:
            if clause.conclusion == query:
                # All premises must recursively be proven True
                all_premises_proven = True
                for premise in clause.premises:
                    if not self.backward_chain(premise, visited.copy()):
                        all_premises_proven = False
                        break
                if all_premises_proven:
                    return True

        return False

# =====================================================================
# 2. PROPOSITIONAL RESOLUTION PROVER (CNF Refutation)
# =====================================================================
Clause = frozenset

def resolve_pair(ci: Clause, cj: Clause) -> Set[Clause]:
    """Resolve two clauses on any complementary literal pair."""
    resolvents = set()
    for literal in ci:
        complement = literal[1:] if literal.startswith('~') else '~' + literal
        if complement in cj:
            # Combine remaining literals
            new_clause = (ci - {literal}) | (cj - {complement})
            resolvents.add(new_clause)
    return resolvents

def pl_resolution(clauses_input: List[List[str]], negated_query: List[str]) -> bool:
    """
    Propositional Resolution Refutation Theorem Prover.
    Returns True if KB |= Query (empty clause derived).
    """
    clauses: Set[Clause] = {frozenset(c) for c in clauses_input}
    clauses.add(frozenset(negated_query))

    new_derived = set()
    step = 0

    while True:
        step += 1
        clause_list = list(clauses)
        pairs = [(clause_list[i], clause_list[j]) 
                 for i in range(len(clause_list)) 
                 for j in range(i + 1, len(clause_list))]

        for ci, cj in pairs:
            resolvents = resolve_pair(ci, cj)
            if frozenset() in resolvents:
                print(f"[Resolution Refutation] Contradiction (Empty Clause derived at step {step})!")
                return True
            new_derived.update(resolvents)

        if new_derived.issubset(clauses):
            return False  # No new clauses can be derived; query not entailed

        clauses.update(new_derived)

# =====================================================================
# DEMONSTRATION HARNESS
# =====================================================================
if __name__ == "__main__":
    print("=" * 68)
    print("DEMO 1: HORN CLAUSE INFERENCE (FORWARD & BACKWARD CHAINING)")
    print("=" * 68)

    kb = KnowledgeBase()
    # Facts
    kb.tell_fact("Colleague(John)")
    kb.tell_fact("HasFever(John)")
    kb.tell_fact("Coughing(John)")

    # Rules
    kb.tell_rule(["HasFever(John)", "Coughing(John)"], "Infected(John)")
    kb.tell_rule(["Infected(John)", "Colleague(John)"], "NeedsQuarantine(John)")
    kb.tell_rule(["NeedsQuarantine(John)"], "AlertManager(John)")

    target = "AlertManager(John)"

    # Forward Chaining
    fc_result, derivation_path = kb.forward_chain(target)
    print(f"Forward Chaining Result for '{target}': {fc_result}")
    print(f"Facts Derivation Sequence: {' -> '.join(derivation_path)}")

    # Backward Chaining
    bc_result = kb.backward_chain(target)
    print(f"Backward Chaining Result for '{target}': {bc_result}\n")

    print("=" * 68)
    print("DEMO 2: PROPOSITIONAL RESOLUTION REFUTATION")
    print("Rules: (P implies Q) and (Q implies R) and P. Query: Prove R.")
    print("=" * 68)

    # KB in CNF:
    # (~P v Q), (~Q v R), (P)
    # Negated query: (~R)
    cnf_kb = [
        ["~P", "Q"],
        ["~Q", "R"],
        ["P"]
    ]
    query_negated = ["~R"]

    proof_success = pl_resolution(cnf_kb, query_negated)
    print(f"Resolution Proof of R: {'SUCCESSFULLY PROVEN' if proof_success else 'FAILED'}")