AlgoVerse

رزولوشن (اثبات با تفکیک)

از دو بند که یکی ℓ و دیگری ¬ℓ را دارد، بند تازه‌ای می‌سازد که بقیه‌ی هر دو را دارد. اگر به بند تهی برسیم، مجموعه‌ی بندها ناسازگار است؛ اثبات با برهان خلف به همین شکل است.

از دو بند p ∨ A و ¬p ∨ B نتیجه می‌شود A ∨ B: اگر p درست باشد، B باید درست باشد و اگر نادرست، A. بند حاصل را تفکیک‌گر (resolvent) می‌گویند.

ادامه‌ی توضیح ↓
ورودی:
clauses="p|q, ~p|r, ~…"خروجی PDF

اثبات q از p ∨ q، ¬p ∨ r و ¬r: نقیض نتیجه (¬q) را اضافه می‌کنیم و به بند تهی می‌رسیم.

  1. def resolution(clauses):
  2. # clauses: "p|q, ~p|r, ~q": a conjunction of disjunctions. Each clause becomes a sorted list of literals.
  3. known = []
  4. rows = [] # for the picture: number, clause, where it came from
  5. for part in clauses.split(","):
  6. lits = sorted(set(x.strip() for x in part.split("|") if x.strip()))
  7. if lits and lits not in known:
  8. known.append(lits)
  9. rows.append([len(rows) + 1, " ∨ ".join(lits), "given"])
  10. count = len(known)
  11. i = 0
  12. while i < len(known):
  13. for j in range(i):
  14. for lit in known[i]:
  15. other = lit[1:] if lit.startswith("~") else "~" + lit
  16. if other not in known[j]:
  17. continue
  18. r = []
  19. for x in known[i] + known[j]:
  20. if x != lit and x != other and x not in r:
  21. r.append(x)
  22. r.sort()
  23. tautology = False
  24. for x in r:
  25. if "~" + x in r:
  26. tautology = True
  27. if tautology or r in known:
  28. continue
  29. known.append(r)
  30. rows.append([len(rows) + 1, " ∨ ".join(r) if r else "□", str(j + 1) + ", " + str(i + 1)])
  31. if not r:
  32. return False
  33. i = i + 1
  34. return True

ناوردا: هر بند تازه نتیجه‌ی منطقی بندهای قبلی است؛ هر مقداردهی که همه‌ی بندها را درست کند، آن را هم درست می‌کند.

شروع اجرا

count—

جدول هنوز خالی است.

متغیرهای محلی

clauses'p|q, ~p|r, ~r, ~q'

نارنجی = در همین گام عوض شد

Call stack

  1. resolution()خط 1
گام ۱ از ۳۲۳
خط سیاه = resolvent · خط نارنجی = گام کلیدیgiven: 0/1 · resolvent: 0/6 · useless: 0/2 · empty_clause: 0/1
    توضیح

    قاعده‌ی تفکیک

    از دو بند p ∨ A و ¬p ∨ B نتیجه می‌شود A ∨ B: اگر p درست باشد، B باید درست باشد و اگر نادرست، A. بند حاصل را تفکیک‌گر (resolvent) می‌گویند.

    اثبات با تفکیک

    برای اثبات اینکه q از فرض‌ها نتیجه می‌شود:

    1. فرض‌ها و نقیض q را به شکل بندی (CNF) بنویس.
    2. تا جایی که می‌شود تفکیک کن.
    3. اگر به بند تهی □ رسیدی (مثلاً از r و ¬r)، مجموعه ناسازگار است، پس q نتیجه می‌شود (برهان خلف).

    تفکیک کامل است: اگر مجموعه‌ای ناسازگار باشد، این روش دیر یا زود بند تهی را می‌سازد. اگر بند تازه‌ای نیاید و بند تهی هم ساخته نشده باشد، مجموعه سازگار است.

    ورودی

    بندها با ویرگول جدا می‌شوند و لیترال‌های هر بند با |؛ ~ یعنی نقیض. متغیرها p، q، r و s اند.