Logic and Proof

from itertools import product

def truth_table(propositions, expr_func, labels):
    """Generate a truth table for a logical expression."""
    n = len(propositions)
    header = " | ".join(labels) + " | Result"
    print(header)
    print("-" * len(header))

    for combo in product([True, False], repeat=n):
        vals = dict(zip(propositions, combo))
        result = expr_func(**vals)
        row = " | ".join(
            f"{vals[p]:^5}" for p in propositions
        ) + f" | {result:^6}"
        print(row)

# --- Basic Operators ---
def AND(p, q):   return p and q
def OR(p, q):    return p or q
def NOT(p):      return not p
def IMPLIES(p, q): return (not p) or q
def IFF(p, q):   return p == q

# --- Verify De Morgan's Laws ---
def verify_demorgan(n_tests=10000):
    import random
    for _ in range(n_tests):
        A = random.randint(0, 1)
        B = random.randint(0, 1)
        lhs_or = not (A or B)
        rhs_or = (not A) and (not B)
        lhs_and = not (A and B)
        rhs_and = (not A) or (not B)
        assert lhs_or == rhs_or, "De Morgan OR violated!"
        assert lhs_and == rhs_and, "De Morgan AND violated!"
    print("De Morgan's laws verified!")

# --- Tautology Checker (brute force) ---
def is_tautology(propositions, expr_func):
    """Check if expr is true for all truth assignments."""
    for combo in product([True, False], repeat=len(propositions)):
        vals = dict(zip(propositions, combo))
        if not expr_func(**vals):
            return False
    return True

# --- SAT Solver (simple DPLL-style) ---
def solve_dpll(clauses, assignment=None):
    """Simple DPLL satisfiability checker.
    clauses: list of tuples, each tuple is a clause (disjunction of literals).
              Literals are (variable_name, is_positive).
    """
    if assignment is None:
        assignment = {}

    # Simplify clauses based on current assignment
    simplified = []
    for clause in clauses:
        satisfied = False
        new_clause = []
        for (var, pos) in clause:
            if var in assignment:
                if assignment[var] == pos:
                    satisfied = True
                    break
            else:
                new_clause.append((var, pos))
        if not satisfied:
            simplified.append(new_clause)

    # Remove clauses that are subsets of others (not needed for correctness)

    # Check for empty clause (contradiction)
    if any(len(c) == 0 for c in simplified):
        return None

    # All clauses satisfied
    if len(simplified) == 0:
        return assignment

    # Unit propagation: if a clause has one literal, assign it
    for clause in simplified:
        if len(clause) == 1:
            var, pos = clause[0]
            if var not in assignment:
                new_assign = dict(assignment)
                new_assign[var] = pos
                return solve_dpll(simplified, new_assign)

    # Choose an unassigned variable and branch
    all_vars = set()
    for clause in simplified:
        for (var, _) in clause:
            all_vars.add(var)
    unassigned = [v for v in all_vars if v not in assignment]
    if not unassigned:
        return assignment

    var = unassigned[0]
    for val in [True, False]:
        new_assign = dict(assignment)
        new_assign[var] = val
        result = solve_dpll(simplified, new_assign)
        if result is not None:
            return result

    return None

# --- CNF Conversion ---
def to_cnf(p, q):
    """Convert P -> Q to CNF and print."""
    # P -> Q ≡ ¬P ∨ Q, which is already CNF
    print(f"  P -> Q ≡ ¬P ∨ Q (CNF)")
    # Verify equivalence
    for pv, qv in product([True, False], repeat=2):
        impl = IMPLIES(pv, qv)
        cnf = OR(NOT(pv), qv)
        assert impl == cnf, f"CNF mismatch for P={pv}, Q={qv}"
    print("  Verified: P -> Q ≡ ¬P ∨ Q")

if __name__ == "__main__":
    print("=== Truth Table: P -> Q ===")
    truth_table(["P", "Q"], IMPLIES, ["P", "Q"])

    print("\n=== Truth Table: P <-> Q ===")
    truth_table(["P", "Q"], IFF, ["P", "Q"])

    print("\n=== De Morgan's Laws ===")
    verify_demorgan()

    print("\n=== Tautology Check ===")
    print(f"P ∨ ¬P is tautology: {is_tautology(['P'], lambda P: OR(P, NOT(P)))}")
    print(f"P ∧ ¬P is tautology: {is_tautology(['P'], lambda P: AND(P, NOT(P)))}")
    print(f"(P -> Q) <-> (¬Q -> ¬P) is tautology: {is_tautology(['P', 'Q'], lambda P, Q: IFF(IMPLIES(P,Q), IMPLIES(NOT(Q), NOT(P))))}")

    print("\n=== CNF Conversion ===")
    to_cnf("P", "Q")

    print("\n=== SAT Solver ===")
    # (P ∨ Q) ∧ (¬P ∨ Q) ∧ (P ∨ ¬Q)
    clauses_sat = [
        [("P", True), ("Q", True)],
        [("P", False), ("Q", True)],
        [("P", True), ("Q", False)],
    ]
    result = solve_dpll(clauses_sat)
    print(f"SAT: {clauses_sat}")
    print(f"Satisfying assignment: {result}")

    # (P) ∧ (¬P) — unsatisfiable
    clauses_unsat = [
        [("P", True)],
        [("P", False)],
    ]
    result = solve_dpll(clauses_unsat)
    print(f"\nSAT: {clauses_unsat}")
    print(f"Result: {result}")