অনুমানের নিয়ম — modus ponens থেকে resolution

১ · Argument কখন valid — premise, উপসংহার আর আকারের নিশ্চয়তা

বাজারঘরের সাপোর্ট টিমে একজন কর্মী রিপোর্ট লিখলেন: “অর্ডার ক্যানসেল হলে টাকা ফেরত যায়। এই অর্ডার ক্যানসেল হয়েছে। অতএব টাকা ফেরত গেছে।” আরেকজন লিখলেন: “অর্ডার ক্যানসেল হলে টাকা ফেরত যায়। এই গ্রাহকের টাকা ফেরত গেছে। অতএব অর্ডার ক্যানসেল হয়েছে।” দুটি দেখতে প্রায় একই রকম। প্রথমটি নির্ভরযোগ্য, দ্বিতীয়টি নয়: টাকা ফেরত যাওয়ার অন্য কারণও থাকতে পারে, যেমন ভুল দামে চার্জ। এই পর্বের বিষয় ঠিক এই পার্থক্য।

খেয়াল করুন, validity premise-গুলোর সত্যতা নিয়ে কিছু বলে না; বলে শুধু আকার নিয়ে। “সব রিকশা উড়তে পারে; আমার বাহন একটি রিকশা; অতএব আমার বাহন উড়তে পারে” — আকার নিখুঁত, তাই valid, যদিও প্রথম premise মিথ্যা। যে argument valid এবং যার সব premise আসলেই সত্য, তাকে বলে sound argument. শুধু sound argument-এর উপসংহার নিশ্চিতভাবে সত্য।

প্রমাণ: P = p₁ ∧ … ∧ p_n লিখি।

1. ∧-এর সংজ্ঞায় একটি সারিতে P সত্য ঠিক তখন, যখন সেই সারিতে প্রতিটি p_i সত্য।
2. →-এর সংজ্ঞায় (পর্ব ০২) P → q একটি সারিতে মিথ্যা ঠিক তখন, যখন সেখানে P সত্য আর q মিথ্যা।
3. ধাপ ১ আর ২ মিলিয়ে: P → q মিথ্যা এমন সারি আছে ⟺ এমন সারি আছে যেখানে সব premise সত্য অথচ q মিথ্যা।
4. বাঁ দিকের অস্বীকার “P → q কোনো সারিতে মিথ্যা নয়” মানে tautology; ডান দিকের অস্বীকার মানে valid. সমান দুটি বাক্যের অস্বীকারও সমান। ∎

এই উপপাদ্য থেকেই যাচাইয়ের একটি সরল যান্ত্রিক পদ্ধতি পাওয়া যায়: সব সারি ঘুরে দেখুন, শুধু সেই সারিগুলোতে চোখ রাখুন যেখানে সব premise সত্য (এদের বলে “গুরুত্বপূর্ণ সারি”), আর দেখুন সেখানে উপসংহার সত্য কি না। একটিও ব্যতিক্রম পেলে সেটিই counterexample. Truth table তৈরি পর্ব ০২-এ দেখেছেন; এখানে একই কৌশল নতুন প্রশ্নে খাটাব।

২ · আটটি অনুমানের নিয়ম — প্রতিটির পেছনে একটি tautology

প্রতিবার ৩২ বা ৬৪ সারির টেবিল বানানো ক্লান্তিকর, আর ২০টি variable-এ অসম্ভব। তাই গণিতবিদরা কয়েকটি ছোট, একবার-যাচাই-করা ছাঁচ রাখেন। প্রতিটি ছাঁচের নাম rule of inference (অনুমানের নিয়ম)। বড় argument-কে এই ছাঁচগুলোর শিকল হিসেবে লিখলে আর টেবিল লাগে না।

Modus ponens (লাতিনে মোটামুটি “স্থাপন করে”) আর modus tollens (“সরিয়ে দিয়ে”) নাম দুটি মধ্যযুগীয় লাতিন যুক্তিশাস্ত্র থেকে এসেছে। Syllogism মানে দুটি premise থেকে একটি উপসংহার টানার ছাঁচ; hypothetical কারণ premise দুটি “যদি… তবে”, disjunctive কারণ একটি premise “অথবা”।

দুটি নিয়মের প্রমাণ

(ক)-এর প্রমাণ (সরাসরি, সারি ধরে):

1. ধরি কোনো সারিতে দুটি premise সত্য: ¬q সত্য, অর্থাৎ q = F; আর p → q সত্য।
2. p = T হলে p → q হতো T → F = F, যা ধাপ ১-এর বিরোধী। তাই p = T হতে পারে না।
3. অতএব p = F, অর্থাৎ ¬p সত্য। সব premise সত্য এমন প্রতিটি সারিতে উপসংহার সত্য, তাই argument valid. ∎

বিকল্প পথ: p → q-এর contrapositive ¬q → ¬p (পর্ব ০২-এর উপপাদ্য ৩.১), তারপর ¬q-এর সঙ্গে modus ponens. অর্থাৎ modus tollens হলো contrapositive-এ modus ponens.

(খ)-এর প্রমাণ (p-এর মান ধরে দুই ক্ষেত্র):

1. ধরি কোনো সারিতে p ∨ q আর ¬p ∨ r দুটোই সত্য। p-এর মান T অথবা F, তৃতীয় কিছু নয়।
2. ক্ষেত্র p = T: তখন ¬p = F, তাই ¬p ∨ r সত্য রাখতে r = T লাগবে। ফলে q ∨ r সত্য।
3. ক্ষেত্র p = F: তখন p ∨ q সত্য রাখতে q = T লাগবে। ফলে q ∨ r সত্য।
4. দুই ক্ষেত্রেই উপসংহার সত্য, আর ক্ষেত্র দুটি সব সম্ভাবনা ঢাকে। ∎

Resolution-এর বিশেষ রূপ দেখুন: r-এর জায়গায় “কিছুই না” (সবসময় মিথ্যা, F) বসালে ¬p ∨ F মানে ¬p, আর উপসংহার q ∨ F মানে q: এটিই disjunctive syllogism. আর p → q-কে ¬p ∨ q লিখলে modus ponens-ও resolution-এর একটি রূপ। এই কারণেই পরে দেখবেন, যন্ত্রে প্রমাণের জন্য শুধু resolution রাখলেই চলে।

প্রতিটি নিয়ম হাতে প্রমাণ করা যায়, কিন্তু কম্পিউটারে সব সারি ঘুরে এক নিমেষে যাচাইও করা যায়। নিচের ব্লক উপপাদ্য ১.১-এর পদ্ধতিটিই চালায়: যে সারিতে সব premise সত্য অথচ উপসংহার মিথ্যা, তা খোঁজে। প্রথমবার চালালে ব্রাউজারে Python (Pyodide) নামতে কয়েক সেকেন্ড লাগে।

from itertools import product

def check(name, names, premises, goal):
    # valid মানে: যে সারিতে সব premise সত্য, সেখানে goal-ও সত্য
    bad = []
    for row in product([True, False], repeat=len(names)):
        v = dict(zip(names, row))
        if all(f(v) for f in premises) and not goal(v):
            bad.append(" ".join(f"{n}={'T' if v[n] else 'F'}" for n in names))
    print(f"{name:23}", "VALID" if not bad else "INVALID, e.g. " + bad[0])

imp = lambda a, b: (not a) or b
p, q, r = (lambda v: v["p"]), (lambda v: v["q"]), (lambda v: v["r"])
nt = lambda f: (lambda v: not f(v))
IF = lambda f, g: (lambda v: imp(f(v), g(v)))
OR = lambda f, g: (lambda v: f(v) or g(v))
AND = lambda f, g: (lambda v: f(v) and g(v))

check("modus ponens", "pq", [p, IF(p, q)], q)
check("modus tollens", "pq", [nt(q), IF(p, q)], nt(p))
check("hypothetical syllogism", "pqr", [IF(p, q), IF(q, r)], IF(p, r))
check("disjunctive syllogism", "pq", [OR(p, q), nt(p)], q)
check("addition", "pq", [p], OR(p, q))
check("simplification", "pq", [AND(p, q)], p)
check("conjunction", "pq", [p, q], AND(p, q))
check("resolution", "pqr", [OR(p, q), OR(nt(p), r)], OR(q, r))
print("--- দেখতে একই রকম, কিন্তু ---")
check("affirming consequent", "pq", [IF(p, q), q], p)
check("denying antecedent", "pq", [IF(p, q), nt(p)], nt(q))
check("p or q, p  =>  not q", "pq", [OR(p, q), p], nt(q))

modus ponens            VALID
modus tollens           VALID
hypothetical syllogism  VALID
disjunctive syllogism   VALID
addition                VALID
simplification          VALID
conjunction             VALID
resolution              VALID
--- দেখতে একই রকম, কিন্তু ---
affirming consequent    INVALID, e.g. p=F q=T
denying antecedent      INVALID, e.g. p=F q=T
p or q, p  =>  not q    INVALID, e.g. p=T q=T

৩ · Fallacy — যে যুক্তি দেখতে ঠিক, কিন্তু ভুল

Fallacy মানে এমন যুক্তির ধরন, যা বিশ্বাসযোগ্য শোনায় কিন্তু valid নয়। গণিতে আর প্রোগ্রামের যুক্তিতে তিনটি সবচেয়ে বেশি দেখা যায়।

• Affirming the consequent (ফলকে সত্য ধরে শর্তে ফেরা): p → q, q ∴ p. এটি আসলে converse q → p-কে মূল বাক্যের সমান ধরা।
• Denying the antecedent (শর্তকে মিথ্যা ধরে ফলকেও মিথ্যা বলা): p → q, ¬p ∴ ¬q. এটি inverse ¬p → ¬q-কে মূল বাক্যের সমান ধরা।
• Begging the question বা circular reasoning (চক্রাকার যুক্তি): যা প্রমাণ করার কথা, সেটিকেই কোনো premise-এ (প্রায়ই অন্য ভাষায়) ধরে নেওয়া। “বাজারঘরের রিভিউ বিশ্বাসযোগ্য, কারণ বাজারঘর কখনো ভুয়া রিভিউ রাখে না” — দ্বিতীয় অংশটিই প্রথম অংশের দাবি।

Circular reasoning-এর একটি মজার বৈশিষ্ট্য: আকারের দিক থেকে এটি প্রায়ই valid (p ∴ p সবসময় valid!)। সমস্যা হলো এটি কিছুই প্রমাণ করে না, কারণ উপসংহারটি premise-এ আগেই বসানো। তাই এটি truth table দিয়ে ধরা যায় না; ধরতে হয় প্রশ্ন করে: “এই premise-টি কি আমার উপসংহার না মেনেই বিশ্বাস করা যায়?”

প্রথম দুটি fallacy truth table দিয়েই ধরা যায়। বাজারঘরের নিরাপত্তা দলের একটি সতর্কবার্তা: “পাসওয়ার্ড ফাঁস হলে অচেনা ডিভাইস থেকে লগইন দেখা যায়। এই অ্যাকাউন্টে অচেনা লগইন দেখা গেছে। অতএব পাসওয়ার্ড ফাঁস হয়েছে।” Argument-টি valid কি না, সারি ধরে দেখুন:

1premise 1: p → q2premise 2: q3∴ p

৪ · Formal proof — প্রতিটি লাইনের কারণসহ

একটি formal proof হলো বাক্যের একটি ক্রমিক তালিকা, যার প্রতিটি লাইন হয় একটি premise, নয়তো আগের কোনো লাইন থেকে একটি অনুমানের নিয়ম খাটিয়ে পাওয়া; শেষ লাইনটি উপসংহার। প্রতিটি লাইনের পাশে কারণ লেখা থাকে: কোন নিয়ম, কোন কোন লাইন থেকে। ফলে যে কেউ, এমনকি একটি প্রোগ্রামও, প্রতিটি লাইন আলাদা করে যাচাই করতে পারে।

বাজারঘরের অপারেশন দলের আজকের পরিস্থিতি:

• H1: “আজ মিরপুরের গুদাম খোলা নেই, এবং ঈদের ভিড় চলছে।” → ¬g ∧ e
• H2: “মিরপুর থেকে পাঠানো হবে শুধু যদি মিরপুরের গুদাম খোলা থাকে।” → m → g (“শুধু যদি”-র দিক পর্ব ০২-এ দেখেছেন)
• H3: “মিরপুর থেকে পাঠানো না হলে উত্তরা থেকে পাঠানো হবে।” → ¬m → u
• উপসংহার: “আজ উত্তরা থেকে পাঠানো হবে।” → u

চার variable-এ টেবিল হলে ১৬ সারি লাগত। নিয়মের শিকলে মাত্র ছয় লাইন। Stepper-এ নামগুলো সংক্ষেপে: simpl. = simplification, MT = modus tollens, MP = modus ponens. “পরে” চাপুন:

1¬g ∧ e  premise2¬g      simpl. 13m → g   premise4¬m      MT 2, 35¬m → u  premise6u       MP 4, 5

নিচের ছবিতে একই প্রমাণকে নির্ভরতার জালে দেখানো হয়েছে: কোন লাইন কোন লাইনের ওপর দাঁড়িয়ে। প্রমাণ পড়ার সময় এই জালটি মাথায় রাখলে বোঝা যায় কোন premise আসলে লাগেনি (এখানে H1-এর e অংশটি)।

প্রমাণের প্রতিটি লাইন ঠিক কি না, যন্ত্রও যাচাই করতে পারে: প্রতিটি লাইন যে লাইনগুলোর উল্লেখ করেছে, সেগুলো সত্য এমন প্রতিটি সারিতে লাইনটি সত্য কি না দেখলেই হয়। নিচের ব্লকে ইচ্ছা করে একটি সপ্তম লাইন যোগ করা হয়েছে, যার বাক্যটি সত্য, কিন্তু কারণটি ভুল:

from itertools import product

imp = lambda a, b: (not a) or b
# g = মিরপুরের গুদাম খোলা, e = ঈদের ভিড়,
# m = মিরপুর থেকে পাঠানো, u = উত্তরা থেকে পাঠানো
proof = [
    ("¬g ∧ e",  lambda g, e, m, u: (not g) and e, "premise", []),
    ("¬g",      lambda g, e, m, u: not g,         "simplification", [1]),
    ("m → g",   lambda g, e, m, u: imp(m, g),     "premise", []),
    ("¬m",      lambda g, e, m, u: not m,         "modus tollens", [2, 3]),
    ("¬m → u",  lambda g, e, m, u: imp(not m, u), "premise", []),
    ("u",       lambda g, e, m, u: u,             "modus ponens", [4, 5]),
    ("¬m",      lambda g, e, m, u: not m,         "from 5 and 6 ?", [5, 6]),
]

def follows(i, refs):
    # উল্লেখ করা লাইনগুলো সত্য এমন প্রতিটি সারিতে লাইন i কি সত্য?
    for row in product([True, False], repeat=4):
        if all(proof[j - 1][1](*row) for j in refs) and not proof[i][1](*row):
            return False
    return True

for i, (text, f, why, refs) in enumerate(proof):
    if why == "premise":
        verdict = "given"
    else:
        verdict = "ok" if follows(i, refs) else "NOT JUSTIFIED"
    cite = ",".join(map(str, refs))
    print(f"{i + 1}. {text:8} {why:16} {cite:4} {verdict}")

1. ¬g ∧ e   premise               given
2. ¬g       simplification   1    ok
3. m → g    premise               given
4. ¬m       modus tollens    2,3  ok
5. ¬m → u   premise               given
6. u        modus ponens     4,5  ok
7. ¬m       from 5 and 6 ?   5,6  NOT JUSTIFIED

প্রমাণ লেখার কয়েকটি কৌশল

• উপসংহার থেকে উল্টো ভাবুন: u চাই; কোন premise-এ u আছে? ¬m → u. তাহলে ¬m চাই; সেটি কোথা থেকে? m → g আর ¬g থেকে। এভাবে পেছনে হেঁটে তারপর সামনে লিখুন।
• যৌগিক premise ভাঙুন: ∧ দেখলে simplification দিয়ে টুকরো করুন।
• দরকারে সমতুল্য রূপ ব্যবহার করুন: p → q-এর জায়গায় ¬p ∨ q বা contrapositive; এগুলো logical equivalence-এর নিয়ম, যা পর্ব ০৩ “Logical equivalence — De Morgan, normal form আর satisfiability”-এ বিস্তারিত।

৫ · Quantifier-ওয়ালা বাক্যে অনুমান — instantiation আর generalization

“বাজারঘরের প্রতিটি প্রিমিয়াম সদস্য ফ্রি ডেলিভারি পান। রিনা প্রিমিয়াম সদস্য। অতএব রিনা ফ্রি ডেলিভারি পান।” এটি propositional logic-এ লেখা যায় না, কারণ “প্রতিটি” লাগে; লাগে পর্ব ০৪ “Predicate logic আর quantifier”-এর ∀ (সব) আর ∃ (অন্তত একটি)। এদের জন্য চারটি অতিরিক্ত নিয়ম আছে:

রিনার উদাহরণে UI আর modus ponens একসঙ্গে খাটে। M(x) = “x প্রিমিয়াম সদস্য”, F(x) = “x ফ্রি ডেলিভারি পান” ধরলে: ∀x (M(x) → F(x)) থেকে UI দিয়ে M(রিনা) → F(রিনা); তারপর M(রিনা)-র সঙ্গে modus ponens দিয়ে F(রিনা)। এই দুই ধাপের জোড়াকে বলে universal modus ponens.

এবার একটু বড় উদাহরণ। Domain = বাজারঘরের সব অর্ডার। W(x) = “x এই সপ্তাহের অর্ডার”, K(x) = “x-এ কুপন লেগেছে”, D(x) = “x ডেলিভারি হয়েছে”।

• Premise ১: এই সপ্তাহের কোনো এক অর্ডারে কুপন লাগেনি: ∃x (W(x) ∧ ¬K(x))
• Premise ২: এই সপ্তাহের প্রতিটি অর্ডার ডেলিভারি হয়েছে: ∀x (W(x) → D(x))
• উপসংহার: ডেলিভারি হয়েছে এমন কোনো অর্ডারে কুপন লাগেনি: ∃x (D(x) ∧ ¬K(x))

প্রমাণ:

1. ∃x (W(x) ∧ ¬K(x)) — premise ১
2. W(a) ∧ ¬K(a) — EI (১), যেখানে a একটি নতুন নাম: “সেই অর্ডারটির নাম দিলাম a”
3. W(a) — simplification (২)
4. ∀x (W(x) → D(x)) — premise ২
5. W(a) → D(a) — UI (৪); a domain-এর একটি উপাদান, তাই বসানো চলে
6. D(a) — modus ponens (৩, ৫)
7. ¬K(a) — simplification (২)
8. D(a) ∧ ¬K(a) — conjunction (৬, ৭)
9. ∃x (D(x) ∧ ¬K(x)) — EG (৮) ∎

লাইনের ক্রম লক্ষ করুন: EI আগে, UI পরে। উল্টো করলে, অর্থাৎ আগে UI দিয়ে কোনো c বসিয়ে পরে EI-তে সেই একই c ব্যবহার করলে, “নতুন নাম” শর্ত ভাঙত। ∃ শুধু বলে “কেউ একজন আছে”, সে কে তা নয়; তাই তাকে আগে থেকে পরিচিত কারও সঙ্গে মিলিয়ে ফেলা যায় না।

Quantifier-ওয়ালা argument-এ truth table চলে না, কারণ domain যেকোনো আকারের, এমনকি অসীম হতে পারে। তবে ছোট domain-এ সব সম্ভাব্য অর্থ ঘুরে counterexample খোঁজা যায়। নিচের ব্লক domain-এর আকার ১, ২ আর ৩ নিয়ে প্রতিটি predicate-এর সব সম্ভাব্য অর্থ পরীক্ষা করে:

from itertools import product

def test(name, k, premises, goal, max_n=3):
    # ছোট সব domain {0..n-1}, আর k-টি predicate-এর সব সম্ভাব্য অর্থ
    checked = 0
    for n in range(1, max_n + 1):
        U = range(n)
        for preds in product(product([True, False], repeat=n), repeat=k):
            checked += 1
            if all(f(U, *preds) for f in premises) and not goal(U, *preds):
                shown = ["".join("T" if b else "F" for b in P) for P in preds]
                print(f"{name}: FAILS at n={n}, predicates {shown}")
                return
    print(f"{name}: no counterexample in {checked} small models")

# W = এই সপ্তাহের অর্ডার, K = কুপন লেগেছে, D = ডেলিভারি হয়েছে
test("coupon argument", 3,
     [lambda U, W, K, D: any(W[x] and not K[x] for x in U),
      lambda U, W, K, D: all((not W[x]) or D[x] for x in U)],
     lambda U, W, K, D: any(D[x] and not K[x] for x in U))

# P = কার্ডে পরিশোধ, Q = ক্যাশে পরিশোধ
test("same-c argument", 2,
     [lambda U, P, Q: any(P[x] for x in U),
      lambda U, P, Q: any(Q[x] for x in U)],
     lambda U, P, Q: any(P[x] and Q[x] for x in U))

coupon argument: no counterexample in 584 small models
same-c argument: FAILS at n=2, predicates ['TF', 'FT']

৬ · Resolution আর refutation — একটিমাত্র নিয়মে প্রমাণ

মানুষ প্রমাণ লেখার সময় আট-দশটি নিয়ম থেকে বেছে নেয়। কম্পিউটারের জন্য এত পছন্দ ঝামেলার: কোন ধাপে কোন নিয়ম? Resolution-এর আকর্ষণ হলো এটি একাই যথেষ্ট, যদি সব বাক্য একটি নির্দিষ্ট আকারে লেখা থাকে।

উপপাদ্য ২.১(খ)-এর প্রমাণ এখানেও হুবহু খাটে (q আর r-এর জায়গায় A আর B-এর ∨), তাই resolution sound: যা বের করে, তা সত্যিই premise থেকে আসে।

এখন প্রমাণ কীভাবে? চালাকিটির নাম resolution refutation, বিরোধ খুঁজে প্রমাণ:

1. KB (জানা বাক্যের সংগ্রহ, knowledge base) ⊨ α প্রমাণ করতে চাই।
2. KB-র সঙ্গে ¬α যোগ করি, সব CNF-এ আনি।
3. বারবার resolution চালাই। □ পেলে KB ∧ ¬α একসঙ্গে অসম্ভব (unsatisfiable).
4. KB সত্য অথচ α মিথ্যা এমন কোনো সারি তাই নেই; অর্থাৎ KB ⊨ α. এটি proof by contradiction-এর যান্ত্রিক রূপ (পর্ব ০৮-এ বিস্তারিত)।

বাজারঘরের নিয়ম: p = “অর্ডার কার্ডে পরিশোধিত”, q = “অর্ডার ক্যাশ অন ডেলিভারিতে”, r = “গ্রাহককে রসিদ পাঠানো হয়”। জানা: প্রতিটি অর্ডার কার্ডে অথবা ক্যাশে (p ∨ q); কার্ডে হলে রসিদ যায় (p → r ≡ ¬p ∨ r); ক্যাশে হলে রসিদ যায় (q → r ≡ ¬q ∨ r). প্রমাণ করতে চাই: রসিদ সবসময় যায় (r).

1C1 {p, q}       KB2C2 {¬p, r}      KB3C3 {¬q, r}      KB4C4 {¬r}         ¬লক্ষ্য5C5 {q, r}       C1 + C26C6 {r}          C5 + C37C7 □            C6 + C4

এই কাজটিই একটি ছোট প্রোগ্রাম করতে পারে: সব জোড়া clause-এ resolution চালাতে থাকে, নতুন কিছু না এলে থামে। □ পেলে প্রমাণ কোন পথে এলো, তা পেছনে হেঁটে ছাপে।

from itertools import combinations
neg = lambda L: L[1:] if L[0] == "~" else "~" + L
show = lambda c: "{" + ", ".join(c).replace("~", "¬") + "}" if c else "□"
key = lambda x: (x.lstrip("~"), x)

def resolvents(a, b):
    for L in a:
        c = tuple(sorted(set(a) - {L} | set(b) - {neg(L)}, key=key))
        if neg(L) in b and not any(neg(x) in c for x in c):  # tautology বাদ
            yield c

def refute(clauses):
    known = [tuple(sorted(c, key=key)) for c in clauses]
    parent = dict.fromkeys(known)
    while True:
        new = []
        for a, b in combinations(known, 2):
            for c in resolvents(a, b):
                if c in parent: continue
                parent[c] = (a, b); new.append(c)
                if c == (): return parent, len(parent)
        if not new: return None, len(parent)
        known += new

def explain(c, parent):
    if parent[c]:
        a, b = parent[c]; explain(a, parent); explain(b, parent)
        print(f"  {show(a)} + {show(b)}  ->  {show(c)}")

# p কার্ডে পরিশোধ, q ক্যাশ অন ডেলিভারি, r রসিদ, s এসএমএস
KB = [["p", "q"], ["~p", "r"], ["~q", "r"]]
for goal in ["r", "s"]:
    parent, n = refute(KB + [[neg(goal)]])
    print(f"goal {goal}: {n} clauses seen,", "PROVED" if parent else "not provable")
    if parent: explain((), parent)

goal r: 12 clauses seen, PROVED
  {p, q} + {¬q, r}  ->  {p, r}
  {¬p, r} + {p, r}  ->  {r}
  {¬r} + {r}  ->  □
goal s: 7 clauses seen, not provable

৭ · Soundness আর completeness — নিয়মের সেট কতটা ভালো

দুটি আলাদা ধারণা গুলিয়ে ফেলা খুব সাধারণ: “⊨” (সত্যের দিক থেকে আসে, truth table দিয়ে সংজ্ঞায়িত) আর “⊢” (নিয়ম খাটিয়ে বের করা যায়)। একটি নিয়মের সেটকে দুই প্রশ্নে বিচার করা হয়:

Soundness প্রমাণ সহজ, আর এই পর্বে আসলে করেই ফেলেছেন: প্রতিটি নিয়ম valid (উপপাদ্য ২.১ আর Python যাচাই), আর valid ধাপের শিকলও valid. Completeness অনেক গভীর। এই পর্বের আটটি নিয়ম একসঙ্গে কোনো পূর্ণাঙ্গ ব্যবস্থা নয়; যেমন “p → q” ধরনের উপসংহার সরাসরি প্রমাণ করতে “ধরে নিয়ে দেখানো” (conditional proof) জাতীয় কৌশল লাগে। পাঠ্যবইয়ের পূর্ণ ব্যবস্থাগুলো (যেমন natural deduction) propositional logic-এ sound আর complete বলে প্রমাণিত।

Resolution-এর ক্ষেত্রটি সূক্ষ্ম। এটি sound, কিন্তু সাধারণ অর্থে complete নয়: p থেকে p ∨ q valid (addition), অথচ শুধু {p} clause থেকে resolution দিয়ে {p, q} বানানো যায় না, কারণ কাটার মতো কোনো জোড়াই নেই। তবে এটি refutation-complete: clause-এর একটি সেট unsatisfiable হলে resolution দিয়ে □ পাওয়া যাবেই। আর KB ⊨ α প্রশ্নকে আমরা সবসময় “KB ∧ ¬α unsatisfiable কি না” প্রশ্নে বদলাই, তাই refutation-completeness-ই যথেষ্ট। এই উপপাদ্যের প্রমাণ এই পর্বে দেওয়া হচ্ছে না; এটি automated reasoning-এর পাঠ্যবইয়ের বিষয় (একটি সাধারণ পথ হলো variable-এর সংখ্যার ওপর induction).

৮ · AI-এর যুগে — AI-এর লেখা প্রমাণ কীভাবে যাচাই করবেন

AI সহকারী formal proof লিখতে পারে, নিয়মের নামও সুন্দর করে বসায়। কিন্তু এই পর্বের বিষয়েই তার ভুলগুলো সবচেয়ে বিপজ্জনক, কারণ ভুল প্রমাণ দেখতে নিখুঁত লাগে। যে ভুলগুলো বেশি দেখা যায়:

AI-এর প্রমাণ হাতে পেলে — যাচাইয়ের চেকলিস্ট

• প্রতিটি লাইন হয় premise, নয়তো উল্লেখিত লাইন থেকে একটি নামযুক্ত নিয়মে এসেছে; উল্লেখিত লাইন আগেই আছে
• প্রতিটি লাইনের ছাঁচ নিয়মের ছাঁচের সঙ্গে মিলিয়েছি, বিশেষ করে → চিহ্নের দিক
• শেষ লাইন হুবহু দাবিটি, তার converse বা দুর্বল রূপ নয়
• Quantifier থাকলে EI-এর নাম নতুন, UG-এর উপাদান ইচ্ছামতো
• Python-এ সব সারি (বা ছোট সব domain) ঘুরে counterexample খুঁজেছি
• উল্লেখ করা উপপাদ্য বা বইয়ের নাম একটি বিশ্বস্ত পাঠ্যবইয়ে মিলিয়েছি

AI agent-এর knowledge base-এ resolution আর inference কীভাবে চলে, তা AI-এর ভিত্তি আর Python for AI কোর্সের পর্ব ৪৫ আর পর্ব ৪৬-এ আছে; এখানে আমরা তার নিচের গণিতটুকু প্রমাণসহ দেখলাম।