AlgoVerse

جدول درستی

برای هر مقداردهی متغیرها، ارزش هر زیرفرمول را از داخل به بیرون حساب می‌کند و در پایان می‌گوید فرمول همیشه درست (راستگو)، همیشه نادرست (تناقض) یا گاهی درست است.

ارزش یک فرمول گزاره‌ای فقط به ارزش متغیرهایش بستگی دارد. با n متغیر، 2^n مقداردهی هست؛ جدول درستی برای هر کدام یک سطر دارد.

ادامه‌ی توضیح ↓
ورودی:
formula="(p>q)=(~q>~p…"خروجی PDF

(p → q) ↔ (¬q → ¬p): یک شرطی با عکس نقیضش هم‌ارز است؛ هر چهار سطر درست‌اند: راستگو.

  1. class Node:
  2. def __init__(self, op, left, right, text):
  3. self.op = op
  4. self.left = left
  5. self.right = right
  6. self.text = text # how the subformula is written
  9. def truth_table(formula):
  10. root = parse(formula)
  11. if root is None:
  12. return None
  13. names = []
  14. columns = []
  15. collect(root, names, columns)
  16. names.sort()
  17. header = names + [c.text for c in columns]
  18. rows = [header]
  19. trues = 0
  20. for m in range(2 ** len(names)):
  21. env = {}
  22. for i in range(len(names)):
  23. env[names[i]] = (m >> (len(names) - 1 - i)) % 2 == 1
  24. row = []
  25. for name in names:
  26. row.append("T" if env[name] else "F")
  27. for c in columns:
  28. env[c.text] = value(c, env)
  29. row.append("T" if env[c.text] else "F")
  30. rows.append(row)
  31. last = env[root.text]
  32. if last:
  33. trues = trues + 1
  34. if trues == 2 ** len(names):
  35. kind = "tautology"
  36. elif trues == 0:
  37. kind = "contradiction"
  38. else:
  39. kind = "contingent"
  40. return kind
  43. def value(c, env):
  44. # Each column only reads columns to its left: its operands were filled in first.
  45. if c.op == "¬":
  46. return not env[c.right.text]
  47. a = env[c.left.text]
  48. b = env[c.right.text]
  49. if c.op == "∧":
  50. return a & b
  51. if c.op == "∨":
  52. return a | b
  53. if c.op == "→":
  54. return (not a) | b
  55. return a == b
  58. def collect(node, names, columns):
  59. # Postorder, so every column comes after the columns it depends on; a repeated subformula gets one column.
  60. if node.op == "var":
  61. if node.text not in names:
  62. names.append(node.text)
  63. return
  64. if node.left is not None:
  65. collect(node.left, names, columns)
  66. collect(node.right, names, columns)
  67. for c in columns:
  68. if c.text == node.text:
  69. return
  70. columns.append(node)
  73. def parse(text):
  74. # ~ not, & and, | or, > implies, = if and only if; from tightest to loosest. > groups to the right.
  75. toks = []
  76. for c in text:
  77. if c != " ":
  78. toks.append(c)
  79. pos = [0]
  80. root = parse_binary(toks, pos, 0)
  81. if root is None or pos[0] != len(toks):
  82. return None
  83. return root
  86. LEVELS = [["=", "↔"], [">", "→"], ["|", "∨"], ["&", "∧"]]
  89. def parse_binary(toks, pos, level):
  90. if level == len(LEVELS):
  91. return parse_not(toks, pos)
  92. sym, op = LEVELS[level]
  93. left = parse_binary(toks, pos, level + 1)
  94. while left is not None and pos[0] < len(toks) and toks[pos[0]] == sym:
  95. pos[0] += 1
  96. right = parse_binary(toks, pos, level if sym == ">" else level + 1)
  97. if right is None:
  98. return None
  99. left = Node(op, left, right, "(" + left.text + " " + op + " " + right.text + ")")
  100. return left
  103. def parse_not(toks, pos):
  104. if pos[0] >= len(toks):
  105. return None
  106. c = toks[pos[0]]
  107. pos[0] += 1
  108. if c == "~":
  109. inner = parse_not(toks, pos)
  110. if inner is None:
  111. return None
  112. return Node("¬", None, inner, "¬" + inner.text)
  113. if c == "(":
  114. inner = parse_binary(toks, pos, 0)
  115. if inner is None or pos[0] >= len(toks) or toks[pos[0]] != ")":
  116. return None
  117. pos[0] += 1
  118. return inner
  119. if c.isalpha():
  120. return Node("var", None, None, c)
  121. return None

ناوردا: هر ستون فقط از ستون‌های سمت چپش استفاده می‌کند؛ پس وقتی به آن می‌رسیم، عملوندهایش پر شده‌اند.

شروع اجرا

trues—
kind—

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

درخت فراخوانی‌های بازگشتی

نارنجی پر = فراخوانی در حال اجرا · حاشیه‌ی نارنجی = هنوز روی پشته · خاکستری = تمام شده

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

formula'(p>q)=(~q>~p)'

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

Call stack

  1. truth_table()خط 9
گام ۱ از ۶۵۵
خط سیاه = row · خط نارنجی = گام کلیدیcolumns: 0/1 · row: 0/4 · tautology: 0/1
    توضیح

    ایده

    ارزش یک فرمول گزاره‌ای فقط به ارزش متغیرهایش بستگی دارد. با n متغیر، 2^n مقداردهی هست؛ جدول درستی برای هر کدام یک سطر دارد.

    برای خوانا بودن، به جز ستون متغیرها، برای هر زیرفرمول هم یک ستون می‌گذاریم، از داخلی‌ترین به بیرونی‌ترین. هر ستون فقط به ستون‌های قبل از خودش نیاز دارد.

    عملگرها

    | نماد ورودی | عملگر | درست است وقتی | |---|---|---| | ~ | ¬ | عملوند نادرست باشد | | & | ∧ | هر دو درست باشند | | \| | ∨ | حداقل یکی درست باشد | | > | → | مقدم نادرست یا تالی درست باشد | | = | ↔ | هر دو هم‌ارزش باشند |

    دسته‌بندی

    • راستگو (tautology): همه‌ی سطرها درست؛ مثلاً قاعده‌های استنتاج.
    • تناقض: هیچ سطری درست نیست.
    • ممکن (contingent): بعضی سطرها.

    دو فرمول هم‌ارزند اگر A ↔ B راستگو باشد.

    ورودی

    متغیرها p، q، r و s اند. ~ از همه قوی‌تر و = از همه ضعیف‌تر است؛ > از راست گروه‌بندی می‌شود.