class Sentence:

    def evaluate(self, model):
        raise NotImplementedError

    def formula(self):
        raise NotImplementedError

    def symbols(self):
        raise NotImplementedError

# <<<CELL>>>

class Symbol(Sentence):

    def __init__(self, name):
        self.name = name

    def __eq__(self, other):
        return isinstance(other, Symbol) and self.name == other.name

    def evaluate(self, model):
        return model[self.name]

    def formula(self):
        return self.name

    def symbols(self):
        return {self.name}

    def __repr__(self):
        return self.name

# <<<CELL>>>

class Not(Sentence):

    def __init__(self, operand):
        self.operand = operand

    def evaluate(self, model):
        return not self.operand.evaluate(model)

    def formula(self):
        return "¬" + self.operand.formula()

    def symbols(self):
        return self.operand.symbols()

# <<<CELL>>>

class And(Sentence):

    def __init__(self, left, right):
        self.left = left
        self.right = right

    def evaluate(self, model):
        return self.left.evaluate(model) and self.right.evaluate(model)

    def formula(self):
        return f"({self.left.formula()} ∧ {self.right.formula()})"

    def symbols(self):
        return self.left.symbols() | self.right.symbols()

# <<<CELL>>>

class Or(Sentence):

    def __init__(self, left, right):
        self.left = left
        self.right = right

    def evaluate(self, model):
        return self.left.evaluate(model) or self.right.evaluate(model)

    def formula(self):
        return f"({self.left.formula()} ∨ {self.right.formula()})"

    def symbols(self):
        return self.left.symbols() | self.right.symbols()

# <<<CELL>>>

class Implication(Sentence):

    def __init__(self, antecedent, consequent):
        self.antecedent = antecedent
        self.consequent = consequent

    def evaluate(self, model):
        return not (self.antecedent.evaluate(model) and not self.consequent.evaluate(model))

    def formula(self):
        return f"({self.antecedent.formula()} → {self.consequent.formula()})"

    def symbols(self):
        return self.antecedent.symbols() | self.consequent.symbols()

# <<<CELL>>>

class Biconditional(Sentence):

    def __init__(self, left, right):
        self.left = left
        self.right = right

    def evaluate(self, model):
        return self.left.evaluate(model) == self.right.evaluate(model)

    def formula(self):
        return f"({self.left.formula()} ↔ {self.right.formula()})"

    def symbols(self):
        return self.left.symbols() | self.right.symbols()

# <<<CELL>>>

P = Symbol("P")
Q = Symbol("Q")
R = Symbol("R")

print(f"P: {P.formula()}")
print(f"Q: {Q.formula()}")
print(f"R: {R.formula()}")

# <<<CELL>>>

model = {
    "P": True,
    "Q": False
}

print(f"P: {P.evaluate(model)}")
print(f"¬P: {Not(P).evaluate(model)}")
print(f"P ∧ Q: {And(P, Q).evaluate(model)}")
print(f"P ∨ Q: {Or(P, Q).evaluate(model)}")
print(f"P → Q: {Implication(P, Q).evaluate(model)}")
print(f"P ↔ Q: {Biconditional(P, Q).evaluate(model)}")

# <<<CELL>>>

def model_check(knowledge, query):

    def check_all(knowledge, query, symbols, model):

        if not symbols:
            if knowledge.evaluate(model):
                return query.evaluate(model)
            return True

        remaining_symbols = list(symbols)
        p = remaining_symbols[0]
        rest_symbols = set(remaining_symbols[1:])

        model_true = model.copy()
        model_true[p] = True

        model_false = model.copy()
        model_false[p] = False

        return check_all(knowledge, query, rest_symbols, model_true) and \
               check_all(knowledge, query, rest_symbols, model_false)

    all_symbols = knowledge.symbols() | query.symbols()

    return check_all(knowledge, query, all_symbols, {})

# <<<CELL>>>

kb = Implication(P, Q)

query = Q

result = model_check(kb, query)

print(f"Knowledge Base: {kb.formula()}")
print(f"Query: {query.formula()}")
print(f"Does the Knowledge Base entail the Query? {result}")

# <<<CELL>>>

kb = And(Implication(P, Q), P)

query = Q

result = model_check(kb, query)

print(f"Knowledge Base: {kb.formula()}")
print(f"Query: {query.formula()}")
print(f"Does the Knowledge Base entail the Query? {result}")

# <<<CELL>>>

kb = And(Or(P, Q), Not(P))

query = Q

result = model_check(kb, query)

print(f"Knowledge Base: {kb.formula()}")
print(f"Query: {query.formula()}")
print(f"Does the Knowledge Base entail the Query? {result}")

# <<<CELL>>>

kb = Biconditional(P, Q)

query = P

result = model_check(kb, query)

print(f"Knowledge Base: {kb.formula()}")
print(f"Query: {query.formula()}")
print(f"Does the Knowledge Base entail the Query? {result}")

# <<<CELL>>>


k_pq = Implication(P, Q)
k_qr = Implication(Q, R)
kb = And(And(k_pq, k_qr), P)

query = R

result = model_check(kb, query)

print(f"Knowledge Base: {kb.formula()}")
print(f"Query: {query.formula()}")
print(f"Does the Knowledge Base entail the Query? {result}")

# <<<CELL>>>

k_pq = Implication(P, Q)
k_qr = Implication(Q, R)
kb = And(k_pq, k_qr)

query = R

result = model_check(kb, query)

print(f"Knowledge Base: {kb.formula()}")
print(f"Query: {query.formula()}")
print(f"Does the Knowledge Base entail the Query? {result}")

# <<<CELL>>>

P = Symbol("P")
Q = Symbol("Q")
R = Symbol("R")

kb = And(
    Implication(P, Q),
    And(P, R)
)

query = Q

result = model_check(kb, query)

print(result)
