1956 - Logic Theorist（邏輯理論家：第一個 AI 程式）#

# 簡化的 Logic Theorist：命題重言式的啟發式搜尋證明
# 公式用巢狀 tuple 表示：('->', A, B)、('~', A)、('v', A, B)、字串=變元

def substitute(formula, p, q):
    """代換：把公式中所有變元 p 換成公式 q"""
    if formula == p:
        return q
    if isinstance(formula, tuple):
        return (formula[0],) + tuple(substitute(f, p, q) for f in formula[1:])
    return formula

def rewrite(formula):
    """Logic Theorist 的替換規則：等價改寫，化簡公式"""
    if not isinstance(formula, tuple):
        return [formula]
    op = formula[0]
    if op == '~':
        inner = rewrite(formula[1])
        results = []
        for f in inner:
            results.append(('~', f))
            if isinstance(f, tuple) and f[0] == '~':   # ~~P => P
                results.append(f[1])
        return results
    if op == '->':
        a, b = formula[1], formula[2]
        results = []
        for fa in rewrite(a):
            for fb in rewrite(b):
                results.append(('->', fa, fb))
                results.append(('v', ('~', fa), fb))   # P->Q => ~P v Q
        return results
    if op == 'v':
        a, b = formula[1], formula[2]
        results = []
        for fa in rewrite(a):
            for fb in rewrite(b):
                results.append(('v', fa, fb))
                results.append(('v', fb, fa))          # 交換律
                results.append(('->', ('~', fa), fb))  # 反向改寫
        return results
    return [formula]

def heuristic_score(formula, goal):
    """啟發式：分數越低 = 越接近目標（與目標的結構差距）"""
    def diff(a, b):
        if a == b:
            return 0
        if isinstance(a, tuple) and isinstance(b, tuple) and a[0] == b[0]:
            return sum(diff(x, y) for x, y in zip(a[1:], b[1:])) + abs(len(a) - len(b))
        return 1
    return min(diff(f, goal) for f in rewrite(formula))

def prove(goal, knowns, max_steps=2000):
    """手段目的分析：比較差距 -> 選規則 -> 遞迴"""
    frontier = list(knowns)
    steps = 0
    while frontier and steps < max_steps:
        frontier.sort(key=lambda f: heuristic_score(f, goal))
        cur = frontier.pop(0)
        steps += 1
        if cur == goal:
            return True, steps
        subs = [(substitute(cur, p, q), p)
                for p in variables(cur) for q in [True, False]]
        frontier.extend(s for s, _ in subs)
    return False, steps

def variables(formula):
    """收集公式中的變元"""
    if isinstance(formula, str):
        return {formula}
    if isinstance(formula, tuple):
        out = set()
        for f in formula[1:]:
            out |= variables(f)
        return out
    return set()

def is_tautology_by_search(goal):
    """目標是重言式？用啟發式搜尋證明 ~goal 恆假（簡化版）"""
    neg = ('~', goal)
    ok, _ = prove(neg, knowns=[])
    return not ok

known = [('->', 'P', 'Q'), 'P', ('->', 'Q', 'R')]

print("Logic Theorist（簡化版）：modus ponens + 代換 + 啟發式")
print("已知：P→Q, Q→R, P")
print("目標：P→R")
# P→R 可由連鎖三段論（~P v Q、~Q v R 改寫後推出）得證
ok, steps = prove(('->', 'P', 'R'), known)
print(f"  證明成功？{ok}（搜尋步數：{steps}）")

print("\n啟發式打分數（與目標 P→R 的結構差距，越低越好）：")
for f in [('->', 'P', 'R'), ('->', 'P', 'Q'), ('~', ('~', ('->', 'P', 'R'))), ('->', 'Q', 'R')]:
    print(f"  {str(f):35s} 分數 = {heuristic_score(f, ('->', 'P', 'R'))}")

print("\n重言式檢定（搜尋版）：")
for g in [('->', 'P', 'P'), ('v', 'P', ('~', 'P')), ('->', 'P', 'Q')]:
    print(f"  {str(g):20s} 是重言式？{is_tautology_by_search(g)}")

print("\n啟發式的威力：")
print("  窮舉搜尋：分支因子 b、深度 d，節點 ~ b^d —— 指數爆炸")
print("  啟發式搜尋：只展開『分數最低』的節點 —— 剪掉絕大部分搜索樹")
print("  → 這就是 Logic Theorist 用幾十步證出羅素數百頁定理的秘密")

Logic Theorist（簡化版）：modus ponens + 代換 + 啟發式
已知：P→Q, Q→R, P
目標：P→R
  證明成功？True（搜尋步數：1）

啟發式打分數（與目標 P→R 的結構差距，越低越好）：
  ('->', 'P', 'R')                    分數 = 0
  ('->', 'P', 'Q')                    分數 = 1
  ('~', ('~', ('->', 'P', 'R')))      分數 = 0
  ('->', 'Q', 'R')                    分數 = 1

重言式檢定（搜尋版）：
  ('->', 'P', 'P')     是重言式？True
  ('v', 'P', ('~', 'P')) 是重言式？True
  ('->', 'P', 'Q')     是重言式？False

啟發式的威力：
  窮舉搜尋：分支因子 b、深度 d，節點 ~ b^d —— 指數爆炸
  啟發式搜尋：只展開『分數最低』的節點 —— 剪掉絕大部分搜索樹
  → 這就是 Logic Theorist 用幾十步證出羅素數百頁定理的秘密