Proof Checker (toy)

কেন এই প্রজেক্ট

Proof Techniques-এর লেসনে আমরা হাতে প্রমাণ লিখেছি — এবং প্রতিবার একটা প্রশ্ন এড়িয়ে গেছি: “এই লাইনটা আগের লাইন থেকে সত্যিই বের হলো, নাকি আমরা শুধু বিশ্বাস করছি যে বের হলো?”

একজন মানুষ প্রুফ পড়ে বলতে পারে “হ্যাঁ, এটা ঠিক মনে হচ্ছে” — কিন্তু “মনে হচ্ছে” গণিতের মান নয়। যাচাইযোগ্যতা-ই প্রমাণের সংজ্ঞা।

এই প্রজেক্টে আপনি এমন একটা প্রোগ্রাম বানাবেন যেটা কোনো semantics বোঝে না, কোনো “common sense” নেই — শুধু যান্ত্রিকভাবে প্রতিটা লাইন একটা fixed rule-set-এর সাথে মিলিয়ে দেখে। এটাই formal proof-এর মূল ধারণা, আর Level 13-এ (Formal methods, Hoare logic, model checking) এই একই idea আরও বড় স্কেলে ফিরে আসবে।

Natural deduction — নিয়মগুলো

প্রতিটা নিয়ম বলে: “এই আকৃতির লাইন(গুলো) আগে থাকলে, এই লাইনটা লেখা বৈধ।” নিয়মটা বাক্যের গঠন দেখে, তার সত্যতা নিয়ে ভাবে না।

নিয়ম	সংক্ষেপ	থেকে	পাওয়া যায়
Modus Ponens	MP	p, p → q	q
Modus Tollens	MT	¬q, p → q	¬p
Conjunction Intro	∧I	p, q	p ∧ q
Conjunction Elim	∧E	p ∧ q	p (বা q)
Disjunction Intro	∨I	p	p ∨ q (যেকোনো q)
Double Negation	DN	¬¬p	p
Hypothetical Syllogism	HS	p → q, q → r	p → r
Disjunctive Syllogism	DS	p ∨ q, ¬p	q

আর দুইটা sub-proof নিয়ম, যেগুলো নতুন assumption খোলে:

• Conditional Proof (CP): p ধরে নিয়ে যদি q প্রমাণ করা যায়, তাহলে (assumption ছাড়াই) p → q লেখা বৈধ।
• Reductio ad Absurdum (RAA): ¬p ধরে নিয়ে যদি একটা contradiction (r ∧ ¬r) পাওয়া যায়, তাহলে p লেখা বৈধ।

এই দুইটাই Proof Techniques লেসনের “direct proof” ও “proof by contradiction”-এর যান্ত্রিক রূপ।

Proof format

1. p -> q            PREMISE
2. q -> r            PREMISE
3. p                 PREMISE
4. q                 MP 1,3
5. r                 MP 2,4

Sub-proof একটা indent ব্লক হিসেবে:

1. p -> q            PREMISE
2. |  p               ASSUME
3. |  q               MP 1,2
4. p -> q            CP 2-3

ধাপে ধাপে

১. ডেটা মডেল

Formula-র জন্য truth-table-generator প্রজেক্টের tokenizer আর parser-ই পুনর্ব্যবহার করুন — ('->' , left, right) স্টাইলের AST।

from dataclasses import dataclass

@dataclass
class Line:
    num: int
    formula: tuple            # AST, parser থেকে
    rule: str                 # 'MP', 'PREMISE', 'ASSUME', ...
    refs: list[int]           # কোন লাইনের উপর নির্ভর করছে
    depth: int                # sub-proof nesting level

২. প্রতিটা rule-এর checker

প্রতিটা checker নেয়: দাবিকৃত refs-এর formula-গুলো আর নতুন formula। শুধু structural মিল দেখে — AST-এর গঠন তুলনা করে।

def check_mp(refs_formulas, new_formula):
    """p, p->q  ⊢  q"""
    for a in refs_formulas:
        for b in refs_formulas:
            if b[0] == '->' and b[1] == a and b[2] == new_formula:
                return True
    return False

def check_mt(refs_formulas, new_formula):
    """¬q, p->q  ⊢  ¬p"""
    if new_formula[0] != 'NOT':
        return False
    p = new_formula[1]
    for a in refs_formulas:            # a = ¬q প্রার্থী
        if a[0] != 'NOT':
            continue
        q = a[1]
        for b in refs_formulas:        # b = p->q প্রার্থী
            if b[0] == '->' and b[1] == p and b[2] == q:
                return True
    return False

def check_and_intro(refs_formulas, new_formula):
    """p, q  ⊢  p∧q"""
    if new_formula[0] != 'AND':
        return False
    p, q = new_formula[1], new_formula[2]
    return p in refs_formulas and q in refs_formulas

def check_and_elim(refs_formulas, new_formula):
    """p∧q  ⊢  p  (বা q)"""
    for a in refs_formulas:
        if a[0] == 'AND' and (a[1] == new_formula or a[2] == new_formula):
            return True
    return False

RULES = {
    'MP': check_mp,
    'MT': check_mt,
    'AND_I': check_and_intro,
    'AND_E': check_and_elim,
    # ... DN, HS, DS, OR_I একই প্যাটার্নে
}

লক্ষ্য করুন — checker-গুলোর কোথাও evaluate() বা truth value নেই। শুধু tuple-এর গঠন মেলানো। এটাই syntactic proof আর semantic truth-এর পার্থক্য, যেটা Proof Techniques লেসনে conceptually বলা হয়েছিল।

৩. পুরো proof verify করা

def verify(lines: list[Line]) -> list[str]:
    errors = []
    formula_of = {}   # line number -> AST

    for ln in lines:
        formula_of[ln.num] = ln.formula
        ref_formulas = [formula_of[r] for r in ln.refs]

        if ln.rule in ('PREMISE', 'ASSUME'):
            continue   # যেকোনো formula assume করা যায়

        checker = RULES.get(ln.rule)
        if checker is None:
            errors.append(f"লাইন {ln.num}: অজানা rule '{ln.rule}'")
            continue

        if not checker(ref_formulas, ln.formula):
            errors.append(
                f"লাইন {ln.num}: '{ln.rule}' rule অনুযায়ী "
                f"লাইন {ln.refs} থেকে এই formula বের হয় না"
            )

    return errors

৪. Sub-proof scoping

CP আর RAA-এর জন্য একটা ASSUME লাইন একটা নতুন scope খোলে, আর সেই scope-এর ভেতরের লাইনগুলো বাইরে থেকে reference করা যাবে না — শুধু scope বন্ধ হওয়ার পরের CP/RAA লাইনটাই বাইরে দৃশ্যমান।

def check_cp(lines, assume_line, conclusion_line, new_formula):
    """ASSUME p ... q  ⊢  p -> q"""
    p = lines[assume_line].formula
    q = lines[conclusion_line].formula
    return (new_formula == ('->', p, q)
            and lines[assume_line].depth == lines[conclusion_line].depth)

এই scoping ঠিক variable scoping বা stack frame lifetime-এর মতোই — Level 4-এ (Operating Systems) আপনি একই ধরনের “কে কাকে দেখতে পারে” প্রশ্ন আবার দেখবেন।

৫. Cross-verification — brute force দিয়ে checker-কে চেক করুন

আপনার checker নিজেই ভুল হতে পারে। তাই truth-table-generator-এর evaluate() ব্যবহার করে একটা স্বাধীন যাচাই যোগ করুন: প্রতিটা premise সত্য এমন সব assignment-এ conclusion-ও কি সত্য?

def semantic_check(premises_ast, conclusion_ast, variables):
    """Brute-force validity check — proof checker-এর সাথে মিলিয়ে দেখুন"""
    from itertools import product
    for combo in product([False, True], repeat=len(variables)):
        env = dict(zip(variables, combo))
        if all(evaluate(p, env) for p in premises_ast):
            if not evaluate(conclusion_ast, env):
                return False, env      # counterexample পাওয়া গেছে
    return True, None

যদি আপনার syntactic checker কোনো proof “বৈধ” বলে কিন্তু semantic_check একটা counterexample খুঁজে পায় — আপনার কোনো rule checker-এ bug আছে। এই দুইটা পদ্ধতি (syntactic proof আর semantic truth-table) একে অপরকে যাচাই করে — এটাই soundness-এর ধারণা, যা যেকোনো formal system-এর সবচেয়ে গুরুত্বপূর্ণ property।

নিজেকে চ্যালেঞ্জ করুন

1. ভালো error message — শুধু “ভুল” না বলে, কোন rule কেন মেলেনি দেখান (যেমন: “MP-এর জন্য p -> q আকৃতির একটা লাইন লাগবে, refs-এ নেই”)
2. সব rule যোগ করুন — DN, HS, DS, OR elimination (case analysis)
3. প্রমাণ থেকে proof-ই generate করুন — ছোট propositional statement দিলে proof search করে দেখান (backward chaining)
4. অপ্রয়োজনীয় লাইন detect করুন — যে লাইন কোনো পরের লাইনে ব্যবহৃত হয়নি সেটা চিহ্নিত করুন
5. Predicate logic পর্যন্ত বাড়ান — ∀/∃ intro-elim rule যোগ করুন (এখানে unification লাগবে — Level 5-এর type inference-এর পূর্বাভাস)

এটা যেখানে গিয়ে মিশবে

এখানে যা শিখলেন	পরে কোথায় লাগবে
Syntactic rule-matching	Level 5 — Type checker (একই প্যাটার্ন, ভিন্ন rule)
Sub-proof scoping	Level 4 — Stack frame, lexical scoping
Soundness cross-check	Level 13 — Formal methods, model checking
Backward proof search	Level 13 — SAT/SMT solver, Prolog-স্টাইল inference
AST pattern matching	Level 5 — Compiler-এর optimization pass