From dc9566306bffe741dd9e87d2e8ba26e88f8bf077 Mon Sep 17 00:00:00 2001 From: Garritt McCune Date: Mon, 8 Feb 2021 00:15:57 -0600 Subject: [PATCH] Initial commit. --- logic.py | 263 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ puzzle.py | 80 +++++++++++++++++ readme.md | 3 + 3 files changed, 346 insertions(+) create mode 100644 logic.py create mode 100644 puzzle.py create mode 100644 readme.md diff --git a/logic.py b/logic.py new file mode 100644 index 0000000..b80a0d6 --- /dev/null +++ b/logic.py @@ -0,0 +1,263 @@ +import itertools + + +class Sentence(): + + def evaluate(self, model): + """Evaluates the logical sentence.""" + raise Exception("nothing to evaluate") + + def formula(self): + """Returns string formula representing logical sentence.""" + return "" + + def symbols(self): + """Returns a set of all symbols in the logical sentence.""" + return set() + + @classmethod + def validate(cls, sentence): + if not isinstance(sentence, Sentence): + raise TypeError("must be a logical sentence") + + @classmethod + def parenthesize(cls, s): + """Parenthesizes an expression if not already parenthesized.""" + def balanced(s): + """Checks if a string has balanced parentheses.""" + count = 0 + for c in s: + if c == "(": + count += 1 + elif c == ")": + if count <= 0: + return False + count -= 1 + return count == 0 + if not len(s) or s.isalpha() or ( + s[0] == "(" and s[-1] == ")" and balanced(s[1:-1]) + ): + return s + else: + return f"({s})" + + +class Symbol(Sentence): + + def __init__(self, name): + self.name = name + + def __eq__(self, other): + return isinstance(other, Symbol) and self.name == other.name + + def __hash__(self): + return hash(("symbol", self.name)) + + def __repr__(self): + return self.name + + def evaluate(self, model): + try: + return bool(model[self.name]) + except KeyError: + raise Exception(f"variable {self.name} not in model") + + def formula(self): + return self.name + + def symbols(self): + return {self.name} + + +class Not(Sentence): + def __init__(self, operand): + Sentence.validate(operand) + self.operand = operand + + def __eq__(self, other): + return isinstance(other, Not) and self.operand == other.operand + + def __hash__(self): + return hash(("not", hash(self.operand))) + + def __repr__(self): + return f"Not({self.operand})" + + def evaluate(self, model): + return not self.operand.evaluate(model) + + def formula(self): + return "¬" + Sentence.parenthesize(self.operand.formula()) + + def symbols(self): + return self.operand.symbols() + + +class And(Sentence): + def __init__(self, *conjuncts): + for conjunct in conjuncts: + Sentence.validate(conjunct) + self.conjuncts = list(conjuncts) + + def __eq__(self, other): + return isinstance(other, And) and self.conjuncts == other.conjuncts + + def __hash__(self): + return hash( + ("and", tuple(hash(conjunct) for conjunct in self.conjuncts)) + ) + + def __repr__(self): + conjunctions = ", ".join( + [str(conjunct) for conjunct in self.conjuncts] + ) + return f"And({conjunctions})" + + def add(self, conjunct): + Sentence.validate(conjunct) + self.conjuncts.append(conjunct) + + def evaluate(self, model): + return all(conjunct.evaluate(model) for conjunct in self.conjuncts) + + def formula(self): + if len(self.conjuncts) == 1: + return self.conjuncts[0].formula() + return " ∧ ".join([Sentence.parenthesize(conjunct.formula()) + for conjunct in self.conjuncts]) + + def symbols(self): + return set.union(*[conjunct.symbols() for conjunct in self.conjuncts]) + + +class Or(Sentence): + def __init__(self, *disjuncts): + for disjunct in disjuncts: + Sentence.validate(disjunct) + self.disjuncts = list(disjuncts) + + def __eq__(self, other): + return isinstance(other, Or) and self.disjuncts == other.disjuncts + + def __hash__(self): + return hash( + ("or", tuple(hash(disjunct) for disjunct in self.disjuncts)) + ) + + def __repr__(self): + disjuncts = ", ".join([str(disjunct) for disjunct in self.disjuncts]) + return f"Or({disjuncts})" + + def evaluate(self, model): + return any(disjunct.evaluate(model) for disjunct in self.disjuncts) + + def formula(self): + if len(self.disjuncts) == 1: + return self.disjuncts[0].formula() + return " ∨ ".join([Sentence.parenthesize(disjunct.formula()) + for disjunct in self.disjuncts]) + + def symbols(self): + return set.union(*[disjunct.symbols() for disjunct in self.disjuncts]) + + +class Implication(Sentence): + def __init__(self, antecedent, consequent): + Sentence.validate(antecedent) + Sentence.validate(consequent) + self.antecedent = antecedent + self.consequent = consequent + + def __eq__(self, other): + return (isinstance(other, Implication) + and self.antecedent == other.antecedent + and self.consequent == other.consequent) + + def __hash__(self): + return hash(("implies", hash(self.antecedent), hash(self.consequent))) + + def __repr__(self): + return f"Implication({self.antecedent}, {self.consequent})" + + def evaluate(self, model): + return ((not self.antecedent.evaluate(model)) + or self.consequent.evaluate(model)) + + def formula(self): + antecedent = Sentence.parenthesize(self.antecedent.formula()) + consequent = Sentence.parenthesize(self.consequent.formula()) + return f"{antecedent} => {consequent}" + + def symbols(self): + return set.union(self.antecedent.symbols(), self.consequent.symbols()) + + +class Biconditional(Sentence): + def __init__(self, left, right): + Sentence.validate(left) + Sentence.validate(right) + self.left = left + self.right = right + + def __eq__(self, other): + return (isinstance(other, Biconditional) + and self.left == other.left + and self.right == other.right) + + def __hash__(self): + return hash(("biconditional", hash(self.left), hash(self.right))) + + def __repr__(self): + return f"Biconditional({self.left}, {self.right})" + + def evaluate(self, model): + return ((self.left.evaluate(model) + and self.right.evaluate(model)) + or (not self.left.evaluate(model) + and not self.right.evaluate(model))) + + def formula(self): + left = Sentence.parenthesize(str(self.left)) + right = Sentence.parenthesize(str(self.right)) + return f"{left} <=> {right}" + + def symbols(self): + return set.union(self.left.symbols(), self.right.symbols()) + + +def model_check(knowledge, query): + """Checks if knowledge base entails query.""" + + def check_all(knowledge, query, symbols, model): + """Checks if knowledge base entails query, given a particular model.""" + + # If model has an assignment for each symbol + if not symbols: + + # If knowledge base is true in model, then query must also be true + if knowledge.evaluate(model): + return query.evaluate(model) + return True + else: + + # Choose one of the remaining unused symbols + remaining = symbols.copy() + p = remaining.pop() + + # Create a model where the symbol is true + model_true = model.copy() + model_true[p] = True + + # Create a model where the symbol is false + model_false = model.copy() + model_false[p] = False + + # Ensure entailment holds in both models + return (check_all(knowledge, query, remaining, model_true) and + check_all(knowledge, query, remaining, model_false)) + + # Get all symbols in both knowledge and query + symbols = set.union(knowledge.symbols(), query.symbols()) + + # Check that knowledge entails query + return check_all(knowledge, query, symbols, dict()) diff --git a/puzzle.py b/puzzle.py new file mode 100644 index 0000000..421f330 --- /dev/null +++ b/puzzle.py @@ -0,0 +1,80 @@ +from logic import * + +AKnight = Symbol("A is a Knight") +AKnave = Symbol("A is a Knave") + +BKnight = Symbol("B is a Knight") +BKnave = Symbol("B is a Knave") + +CKnight = Symbol("C is a Knight") +CKnave = Symbol("C is a Knave") + +# Puzzle 0 +# A says "I am both a knight and a knave." +knowledge0 = And( + Or(AKnave, AKnight), + And(AKnave, Not(AKnight)), + Implication(And(AKnight, AKnave), AKnave) +) + +# Puzzle 1 +# A says "We are both knaves." +# B says nothing. +knowledge1 = And( + Or(AKnave, AKnight), + Or(BKnave, BKnight), + Or(And(AKnave, BKnight), And(AKnave, BKnave)), + Implication(And(AKnave, BKnave), And(AKnave, BKnight)) +) + +# Puzzle 2 +# A says "We are the same kind." +# B says "We are of different kinds." +knowledge2 = And( + Or(And(AKnave, BKnave), And(AKnight, BKnight), And(AKnave, BKnight)), + Biconditional(AKnave, Not(AKnight)), + Biconditional(BKnave, Not(BKnight)), + Implication(AKnave, Not(And(AKnave, BKnave))), + Implication(BKnight, And(AKnave, BKnight)) +) + +# Puzzle 3 +# A says either "I am a knight." or "I am a knave.", but you don't know which. +# B says "A said 'I am a knave'." +# B says "C is a knave." +# C says "A is a knight." +knowledge3 = And( + Or(AKnave, AKnight), + Or(BKnave, BKnight), + Or(CKnave, CKnight), + Biconditional(AKnave, Not(AKnight)), + Biconditional(BKnave, Not(BKnight)), + Biconditional(CKnave, Not(CKnight)), + + Implication(AKnave, Not(AKnave)), + Implication(BKnight, And(AKnave, CKnave)), + Implication(BKnave, And(AKnight, CKnight)), + Implication(CKnight, And(AKnight, BKnave)) +) + + +def main(): + symbols = [AKnight, AKnave, BKnight, BKnave, CKnight, CKnave] + puzzles = [ + ("Puzzle 0", knowledge0), + ("Puzzle 1", knowledge1), + ("Puzzle 2", knowledge2), + ("Puzzle 3", knowledge3) + ] + for puzzle, knowledge in puzzles: + print(puzzle) + if len(knowledge.conjuncts) == 0: + print(" Not yet implemented.") + else: + for symbol in symbols: + if model_check(knowledge, symbol): + print(f" {symbol}") + + +if __name__ == "__main__": + main() diff --git a/readme.md b/readme.md new file mode 100644 index 0000000..994b53c --- /dev/null +++ b/readme.md @@ -0,0 +1,3 @@ +Homework that I did for an AI class that Harvard offered. Sadly I +never got a chance to finish said class, but I figured these early projects +would be worth archiving.