真理計算ができるだけのスクリプト

propositions.py

from abc import ABC, abstractmethod


class Proposition(ABC):
  def __and__(self, other):
    return CompositeProposition('and', self, other)

  def __or__(self, other):
    return CompositeProposition('or', self, other)

  def __invert__(self):
    return CompositeProposition('not', self)

  def __eq__(self, other):
    return CompositeProposition('iff', self, other)

  def __repr__(self):
    return str(self)

  def implies(self, other):
    return CompositeProposition('imply', self, other)

  @abstractmethod
  def get_truth_table(self):
    pass

  @abstractmethod
  def write_truth_table(self):
    pass

  @abstractmethod
  def is_equivalent(self, other):
    pass

  @abstractmethod
  def get_free_terms(self):
    pass

  @abstractmethod
  def calculate(self, env):
    pass

  @abstractmethod
  def simplify(self):
    pass

class CompositeProposition(Proposition):
  def __init__(self, op, left, right=None):
    self.op = op
    self.left = left
    self.right = right

  def __str__(self):
    if self.op == 'and':
      return f"({self.left} \\wedge {self.right})"
    if self.op == 'or':
      return f"({self.left} \\vee {self.right})"
    if self.op == 'not':
      return f"(\\lnot {self.left})"
    if self.op == 'iff':
      return f"({self.left} \\equiv {self.right})"
    if self.op == 'imply':
      return f"({self.left} \\rightarrow {self.right})"

  def calculate(self, env):
    if self.op == 'and':
      return self.left.calculate(env) and self.right.calculate(env)
    if self.op == 'or':
      return self.left.calculate(env) or self.right.calculate(env)
    if self.op == 'not':
      return not self.left.calculate(env)
    if self.op == 'iff':
      return self.left.calculate(env) == self.right.calculate(env)
    if self.op == 'imply':
      left = self.left.calculate(env)
      right = self.right.calculate(env)
      return not left or right

  def get_truth_table(self):
    frees = list(set(self.get_free_terms()))
    frees.sort()
    envs = [{}]

    for free in frees:
      next = []
      for env in envs:
        t = env.copy()
        f = env.copy()
        t[free] = True
        f[free] = False
        next.append(t)
        next.append(f)
      envs = next

    for env in envs:
      env['$result'] = self.calculate(env)

    frees.append('result')

    return frees, envs

  def write_truth_table(self):
    frees, envs = self.get_truth_table()

    column_width = max(len(f) for f in frees)
    header = f"| {' | '.join(f.ljust(column_width) for f in frees)} |"
    width = len(header)
    spacer = f"+{'-' * (width - 2)}+"
    header = f"{spacer}\n{header}\n{spacer}"
    print(header)

    for env in envs:
      print(f"| {' | '.join(('T' if e else 'F').ljust(column_width) for e in env.values())} |")
    print(spacer)

  def get_free_terms(self):
    terms = self.left.get_free_terms()

    if self.right is not None:
      terms += self.right.get_free_terms()

    return terms

  def is_equivalent(self, other):
    _, my_truth = self.get_truth_table()
    _, other_truth = other.get_truth_table()
    if len(my_truth) != len(other_truth):
      return False

    for i, j in zip(my_truth, other_truth):
      if tuple(i.values()) != tuple(j.values()):
        return False

    return True

  def simplify(self):
    left = self.left.simplify()
    right = None

    if self.right is not None:
      right = self.right.simplify()

    if self.op == 'imply':
      return (~left) | right
    if self.op == 'iff':
      return ((~left) | right) & ((~right) | left)
    if (self.op == 'not' and
        (hasattr(self.left, 'op')
         and self.left.op == 'not')):
      return self.left.left

    return CompositeProposition(self.op, left, right)

class AtomicProposition(Proposition):
  __objects__ = {}

  def __new__(self, name, value: bool=None):
    if name in self.__objects__:
      self = self.__objects__[name]
      self.value = value

    else:
      cls = self
      self = object.__new__(self)
      cls.__objects__[name] = self
      self.__init__(name, value)

    return self

  def __init__(self, name, value: bool=None):
    self.name = name
    self.value = value

  def __str__(self):
    if self.value is None:
      return self.name
    return '1' if self.value else '0'

  def __hash__(self):
    return hash(self.name)

  def get_free_terms(self):
    if self.value is None:
      return [self.name]
    return []

  def calculate(self, env):
    if self.value is None:
      return env.get(self.name, False)
    return self.value

  def get_truth_table(self):
    return (
      [self.name],
      [
        {self.name: True, '$result': True},
        {self.name: False, '$result': False}
      ])

  def is_equivalent(self, other):
    if isinstance(other, AtomicProposition):
      return other.value is self.value

    return other.is_equivalent(self)

  def write_truth_table(self):
    col_width = len(self.name)
    spacer = f"+{'-' * (col_width + 2)}+"
    if self.value is None:
      print(f"{spacer}\n"
            f"| {self.name} |\n"
            f"{spacer}\n"
            f"| {'T'.ljust(col_width)} |\n"
            f"| {'F'.ljust(col_width)} |\n"
            f"{spacer}\n")
    print(f"{spacer}\n"
          f"| {self.name} |\n"
          f"{spacer}\n"
          f"| {['F', 'T'][self.value].ljust(col_width)} |\n"
          f"{spacer}\n")

  def simplify(self):
    return self

def p(name: str):
  return AtomicProposition(name)

def const(name: str, value: bool):
  return AtomicProposition(name, value)

T = const('T', True)
F = const('T', False)

usage.py

from propositions import p

P = p('P')
Q = p('Q')
R = p('R')

print((P & Q).implies(R))
# -> ((P \wedge Q) \rightarrow R)
(P & Q).implies(R).write_truth_table()
# +-----------------------------------+
# | P      | Q      | R      | result |
# +-----------------------------------+
# | T      | T      | T      | T      |
# | T      | T      | F      | F      |
# | T      | F      | T      | T      |
# | T      | F      | F      | T      |
# | F      | T      | T      | T      |
# | F      | T      | F      | T      |
# | F      | F      | T      | T      |
# | F      | F      | F      | T      |
# +-----------------------------------+

# 論理否定
print(~P)

# 論理和
print(P | Q)

# 論理積
print(P & Q)

# 同値
print(P == Q)

# 含意
print(P.implies(Q))

# 同値性の検証
print(P.implies(Q).is_equivalent(~P | Q))