From 0521014b466b17207055b21457c9f78b27ce5246 Mon Sep 17 00:00:00 2001 From: Joshua Mayhugh <123776276+jmayhugh1@users.noreply.github.com> Date: Mon, 17 Feb 2025 19:49:18 -0600 Subject: [PATCH 1/3] started ppsat.py --- agents.ipynb | 514 ++++++++++- logic.ipynb | 4 +- logic4e_modify_v01.py | 1969 +++++++++++++++++++++++++++++++++++++++++ ppsat.py | 155 ++++ 4 files changed, 2611 insertions(+), 31 deletions(-) create mode 100644 logic4e_modify_v01.py create mode 100644 ppsat.py diff --git a/agents.ipynb b/agents.ipynb index 636df75e3..76b35c41a 100644 --- a/agents.ipynb +++ b/agents.ipynb @@ -11,7 +11,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 2, "metadata": {}, "outputs": [], "source": [ @@ -43,9 +43,152 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 3, "metadata": {}, - "outputs": [], + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
class Agent(Thing):\n",
+       "    """An Agent is a subclass of Thing with one required instance attribute \n",
+       "    (aka slot), .program, which should hold a function that takes one argument,\n",
+       "    the percept, and returns an action. (What counts as a percept or action \n",
+       "    will depend on the specific environment in which the agent exists.)\n",
+       "    Note that 'program' is a slot, not a method. If it were a method, then the\n",
+       "    program could 'cheat' and look at aspects of the agent. It's not supposed\n",
+       "    to do that: the program can only look at the percepts. An agent program\n",
+       "    that needs a model of the world (and of the agent itself) will have to\n",
+       "    build and maintain its own model. There is an optional slot, .performance,\n",
+       "    which is a number giving the performance measure of the agent in its\n",
+       "    environment."""\n",
+       "\n",
+       "    def __init__(self, program=None):\n",
+       "        self.alive = True\n",
+       "        self.bump = False\n",
+       "        self.holding = []\n",
+       "        self.performance = 0\n",
+       "        if program is None or not isinstance(program, collections.abc.Callable):\n",
+       "            print("Can't find a valid program for {}, falling back to default.".format(self.__class__.__name__))\n",
+       "\n",
+       "            def program(percept):\n",
+       "                return eval(input('Percept={}; action? '.format(percept)))\n",
+       "\n",
+       "        self.program = program\n",
+       "\n",
+       "    def can_grab(self, thing):\n",
+       "        """Return True if this agent can grab this thing.\n",
+       "        Override for appropriate subclasses of Agent and Thing."""\n",
+       "        return False\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], "source": [ "psource(Agent)" ] @@ -75,9 +218,222 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 4, "metadata": {}, - "outputs": [], + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
class Environment:\n",
+       "    """Abstract class representing an Environment. 'Real' Environment classes\n",
+       "    inherit from this. Your Environment will typically need to implement:\n",
+       "        percept:           Define the percept that an agent sees.\n",
+       "        execute_action:    Define the effects of executing an action.\n",
+       "                           Also update the agent.performance slot.\n",
+       "    The environment keeps a list of .things and .agents (which is a subset\n",
+       "    of .things). Each agent has a .performance slot, initialized to 0.\n",
+       "    Each thing has a .location slot, even though some environments may not\n",
+       "    need this."""\n",
+       "\n",
+       "    def __init__(self):\n",
+       "        self.things = []\n",
+       "        self.agents = []\n",
+       "\n",
+       "    def thing_classes(self):\n",
+       "        return []  # List of classes that can go into environment\n",
+       "\n",
+       "    def percept(self, agent):\n",
+       "        """Return the percept that the agent sees at this point. (Implement this.)"""\n",
+       "        raise NotImplementedError\n",
+       "\n",
+       "    def execute_action(self, agent, action):\n",
+       "        """Change the world to reflect this action. (Implement this.)"""\n",
+       "        raise NotImplementedError\n",
+       "\n",
+       "    def default_location(self, thing):\n",
+       "        """Default location to place a new thing with unspecified location."""\n",
+       "        return None\n",
+       "\n",
+       "    def exogenous_change(self):\n",
+       "        """If there is spontaneous change in the world, override this."""\n",
+       "        pass\n",
+       "\n",
+       "    def is_done(self):\n",
+       "        """By default, we're done when we can't find a live agent."""\n",
+       "        return not any(agent.is_alive() for agent in self.agents)\n",
+       "\n",
+       "    def step(self):\n",
+       "        """Run the environment for one time step. If the\n",
+       "        actions and exogenous changes are independent, this method will\n",
+       "        do. If there are interactions between them, you'll need to\n",
+       "        override this method."""\n",
+       "        if not self.is_done():\n",
+       "            actions = []\n",
+       "            for agent in self.agents:\n",
+       "                if agent.alive:\n",
+       "                    actions.append(agent.program(self.percept(agent)))\n",
+       "                else:\n",
+       "                    actions.append("")\n",
+       "            for (agent, action) in zip(self.agents, actions):\n",
+       "                self.execute_action(agent, action)\n",
+       "            self.exogenous_change()\n",
+       "\n",
+       "    def run(self, steps=1000):\n",
+       "        """Run the Environment for given number of time steps."""\n",
+       "        for step in range(steps):\n",
+       "            if self.is_done():\n",
+       "                return\n",
+       "            self.step()\n",
+       "\n",
+       "    def list_things_at(self, location, tclass=Thing):\n",
+       "        """Return all things exactly at a given location."""\n",
+       "        if isinstance(location, numbers.Number):\n",
+       "            return [thing for thing in self.things\n",
+       "                    if thing.location == location and isinstance(thing, tclass)]\n",
+       "        return [thing for thing in self.things\n",
+       "                if all(x == y for x, y in zip(thing.location, location)) and isinstance(thing, tclass)]\n",
+       "\n",
+       "    def some_things_at(self, location, tclass=Thing):\n",
+       "        """Return true if at least one of the things at location\n",
+       "        is an instance of class tclass (or a subclass)."""\n",
+       "        return self.list_things_at(location, tclass) != []\n",
+       "\n",
+       "    def add_thing(self, thing, location=None):\n",
+       "        """Add a thing to the environment, setting its location. For\n",
+       "        convenience, if thing is an agent program we make a new agent\n",
+       "        for it. (Shouldn't need to override this.)"""\n",
+       "        if not isinstance(thing, Thing):\n",
+       "            thing = Agent(thing)\n",
+       "        if thing in self.things:\n",
+       "            print("Can't add the same thing twice")\n",
+       "        else:\n",
+       "            thing.location = location if location is not None else self.default_location(thing)\n",
+       "            self.things.append(thing)\n",
+       "            if isinstance(thing, Agent):\n",
+       "                thing.performance = 0\n",
+       "                self.agents.append(thing)\n",
+       "\n",
+       "    def delete_thing(self, thing):\n",
+       "        """Remove a thing from the environment."""\n",
+       "        try:\n",
+       "            self.things.remove(thing)\n",
+       "        except ValueError as e:\n",
+       "            print(e)\n",
+       "            print("  in Environment delete_thing")\n",
+       "            print("  Thing to be removed: {} at {}".format(thing, thing.location))\n",
+       "            print("  from list: {}".format([(thing, thing.location) for thing in self.things]))\n",
+       "        if thing in self.agents:\n",
+       "            self.agents.remove(thing)\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], "source": [ "psource(Environment)" ] @@ -114,9 +470,17 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 5, "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Can't find a valid program for BlindDog, falling back to default.\n" + ] + } + ], "source": [ "class BlindDog(Agent):\n", " def eat(self, thing):\n", @@ -137,9 +501,17 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 6, "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "True\n" + ] + } + ], "source": [ "print(dog.alive)" ] @@ -163,7 +535,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 8, "metadata": {}, "outputs": [], "source": [ @@ -217,7 +589,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 9, "metadata": {}, "outputs": [], "source": [ @@ -264,7 +636,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 10, "metadata": {}, "outputs": [], "source": [ @@ -287,9 +659,21 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 11, "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "BlindDog decided to move down at location: 1\n", + "BlindDog decided to move down at location: 2\n", + "BlindDog decided to move down at location: 3\n", + "BlindDog decided to move down at location: 4\n", + "BlindDog ate Food at location: 5\n" + ] + } + ], "source": [ "park = Park()\n", "dog = BlindDog(program)\n", @@ -313,9 +697,19 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 12, "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "BlindDog decided to move down at location: 5\n", + "BlindDog decided to move down at location: 6\n", + "BlindDog drank Water at location: 7\n" + ] + } + ], "source": [ "park.run(5)" ] @@ -329,9 +723,25 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 13, "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "BlindDog decided to move down at location: 7\n", + "BlindDog decided to move down at location: 8\n", + "BlindDog decided to move down at location: 9\n", + "BlindDog decided to move down at location: 10\n", + "BlindDog decided to move down at location: 11\n", + "BlindDog decided to move down at location: 12\n", + "BlindDog decided to move down at location: 13\n", + "BlindDog decided to move down at location: 14\n", + "BlindDog drank Water at location: 15\n" + ] + } + ], "source": [ "park.add_thing(water, 15)\n", "park.run(10)" @@ -357,7 +767,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 14, "metadata": {}, "outputs": [], "source": [ @@ -423,9 +833,22 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 15, "metadata": {}, - "outputs": [], + "outputs": [ + { + "data": { + "text/html": [ + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], "source": [ "park = Park2D(5,20, color={'BlindDog': (200,0,0), 'Water': (0, 200, 200), 'Food': (230, 115, 40)}) # park width is set to 5, and height to 20\n", "dog = BlindDog(program)\n", @@ -482,7 +905,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 16, "metadata": {}, "outputs": [], "source": [ @@ -553,7 +976,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 17, "metadata": {}, "outputs": [], "source": [ @@ -618,9 +1041,22 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 18, "metadata": {}, - "outputs": [], + "outputs": [ + { + "data": { + "text/html": [ + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], "source": [ "park = Park2D(5,5, color={'EnergeticBlindDog': (200,0,0), 'Water': (0, 200, 200), 'Food': (230, 115, 40)})\n", "dog = EnergeticBlindDog(program)\n", @@ -654,7 +1090,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 21, "metadata": {}, "outputs": [], "source": [ @@ -698,7 +1134,27 @@ "cell_type": "code", "execution_count": null, "metadata": {}, - "outputs": [], + "outputs": [ + { + "data": { + "text/html": [ + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[[], [], [], [], [None]]\n" + ] + } + ], "source": [ "step()" ] @@ -713,7 +1169,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": ".venv", "language": "python", "name": "python3" }, @@ -727,7 +1183,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4" + "version": "3.13.2" } }, "nbformat": 4, diff --git a/logic.ipynb b/logic.ipynb index 062ffede2..126106865 100644 --- a/logic.ipynb +++ b/logic.ipynb @@ -4982,7 +4982,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": ".venv", "language": "python", "name": "python3" }, @@ -4996,7 +4996,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.1" + "version": "3.13.2" } }, "nbformat": 4, diff --git a/logic4e_modify_v01.py b/logic4e_modify_v01.py new file mode 100644 index 000000000..8157bc20d --- /dev/null +++ b/logic4e_modify_v01.py @@ -0,0 +1,1969 @@ +"""Representations and Inference for Logic (Chapters 7-10) + +Covers both Propositional and First-Order Logic. First we have four +important data types: + + KB Abstract class holds a knowledge base of logical expressions + KB_Agent Abstract class subclasses agents.Agent + Expr A logical expression, imported from utils.py + substitution Implemented as a dictionary of var:value pairs, {x:1, y:x} + +Be careful: some functions take an Expr as argument, and some take a KB. + +Logical expressions can be created with Expr or expr, imported from utils, TODO +or with expr, which adds the capability to write a string that uses +the connectives ==>, <==, <=>, or <=/=>. But be careful: these have the +operator precedence of commas; you may need to add parents to make precedence work. +See logic.ipynb for examples. + +Then we implement various functions for doing logical inference: + + pl_true Evaluate a propositional logical sentence in a model + tt_entails Say if a statement is entailed by a KB + pl_resolution Do resolution on propositional sentences + dpll_satisfiable See if a propositional sentence is satisfiable + WalkSAT Try to find a solution for a set of clauses + +And a few other functions: + + to_cnf Convert to conjunctive normal form + unify Do unification of two FOL sentences + diff, simp Symbolic differentiation and simplification +""" +import itertools +import random +from collections import defaultdict + +from agents import Agent, Glitter, Bump, Stench, Breeze, Scream +from search import astar_search, PlanRoute +from utils4e import remove_all, unique, first, probability, isnumber, issequence, Expr, expr, subexpressions + + +# ______________________________________________________________________________ +# Chapter 7 Logical Agents +# 7.1 Knowledge Based Agents + + +class KB: + """ + A knowledge base to which you can tell and ask sentences. + To create a KB, subclass this class and implement tell, ask_generator, and retract. + Ask_generator: + For a Propositional Logic KB, ask(P & Q) returns True or False, but for an + FOL KB, something like ask(Brother(x, y)) might return many substitutions + such as {x: Cain, y: Abel}, {x: Abel, y: Cain}, {x: George, y: Jeb}, etc. + So ask_generator generates these one at a time, and ask either returns the + first one or returns False. + """ + + def __init__(self, sentence=None): + raise NotImplementedError + + def tell(self, sentence): + """Add the sentence to the KB.""" + raise NotImplementedError + + def ask(self, query): + """Return a substitution that makes the query true, or, failing that, return False.""" + return first(self.ask_generator(query), default=False) + + def ask_generator(self, query): + """Yield all the substitutions that make query true.""" + raise NotImplementedError + + def retract(self, sentence): + """Remove sentence from the KB.""" + raise NotImplementedError + + +class PropKB(KB): + """A KB for propositional logic. Inefficient, with no indexing.""" + + def __init__(self, sentence=None): + self.clauses = [] + if sentence: + self.tell(sentence) + + def tell(self, sentence): + """Add the sentence's clauses to the KB.""" + self.clauses.extend(conjuncts(to_cnf(sentence))) + + def ask_generator(self, query): + """Yield the empty substitution {} if KB entails query; else no results.""" + if tt_entails(Expr('&', *self.clauses), query): + yield {} + + def ask_if_true(self, query): + """Return True if the KB entails query, else return False.""" + for _ in self.ask_generator(query): + return True + return False + + def retract(self, sentence): + """Remove the sentence's clauses from the KB.""" + for c in conjuncts(to_cnf(sentence)): + if c in self.clauses: + self.clauses.remove(c) + + +def KB_AgentProgram(KB): + """A generic logical knowledge-based agent program. [Figure 7.1]""" + steps = itertools.count() + + def program(percept): + t = next(steps) + KB.tell(make_percept_sentence(percept, t)) + action = KB.ask(make_action_query(t)) + KB.tell(make_action_sentence(action, t)) + return action + + def make_percept_sentence(percept, t): + return Expr("Percept")(percept, t) + + def make_action_query(t): + return expr("ShouldDo(action, {})".format(t)) + + def make_action_sentence(action, t): + return Expr("Did")(action[expr('action')], t) + + return program + + +# _____________________________________________________________________________ +# 7.2 The Wumpus World + + +# Expr functions for WumpusKB and HybridWumpusAgent + + +def facing_east(time): + return Expr('FacingEast', time) + + +def facing_west(time): + return Expr('FacingWest', time) + + +def facing_north(time): + return Expr('FacingNorth', time) + + +def facing_south(time): + return Expr('FacingSouth', time) + + +def wumpus(x, y): + return Expr('W', x, y) + + +def pit(x, y): + return Expr('P', x, y) + + +def breeze(x, y): + return Expr('B', x, y) + + +def stench(x, y): + return Expr('S', x, y) + + +def wumpus_alive(time): + return Expr('WumpusAlive', time) + + +def have_arrow(time): + return Expr('HaveArrow', time) + + +def percept_stench(time): + return Expr('Stench', time) + + +def percept_breeze(time): + return Expr('Breeze', time) + + +def percept_glitter(time): + return Expr('Glitter', time) + + +def percept_bump(time): + return Expr('Bump', time) + + +def percept_scream(time): + return Expr('Scream', time) + + +def move_forward(time): + return Expr('Forward', time) + + +def shoot(time): + return Expr('Shoot', time) + + +def turn_left(time): + return Expr('TurnLeft', time) + + +def turn_right(time): + return Expr('TurnRight', time) + + +def ok_to_move(x, y, time): + return Expr('OK', x, y, time) + + +def location(x, y, time=None): + if time is None: + return Expr('L', x, y) + else: + return Expr('L', x, y, time) + + +# Symbols + + +def implies(lhs, rhs): + return Expr('==>', lhs, rhs) + + +def equiv(lhs, rhs): + return Expr('<=>', lhs, rhs) + + +# Helper Function + + +def new_disjunction(sentences): + t = sentences[0] + for i in range(1, len(sentences)): + t |= sentences[i] + return t + + +# ______________________________________________________________________________ +# 7.4 Propositional Logic + + +def is_symbol(s): + """A string s is a symbol if it starts with an alphabetic char. + >>> is_symbol('R2D2') + True + """ + return isinstance(s, str) and s[:1].isalpha() + + +def is_var_symbol(s): + """A logic variable symbol is an initial-lowercase string. + >>> is_var_symbol('EXE') + False + """ + return is_symbol(s) and s[0].islower() + + +def is_prop_symbol(s): + """A proposition logic symbol is an initial-uppercase string. + >>> is_prop_symbol('exe') + False + """ + return is_symbol(s) and s[0].isupper() + + +def variables(s): + """Return a set of the variables in expression s. + >>> variables(expr('F(x, x) & G(x, y) & H(y, z) & R(A, z, 2)')) == {x, y, z} + True + """ + return {x for x in subexpressions(s) if is_variable(x)} + + +def is_definite_clause(s): + """ + Returns True for exprs s of the form A & B & ... & C ==> D, + where all literals are positive. In clause form, this is + ~A | ~B | ... | ~C | D, where exactly one clause is positive. + >>> is_definite_clause(expr('Farmer(Mac)')) + True + """ + if is_symbol(s.op): + return True + elif s.op == '==>': + antecedent, consequent = s.args + return (is_symbol(consequent.op) and + all(is_symbol(arg.op) for arg in conjuncts(antecedent))) + else: + return False + + +def parse_definite_clause(s): + """Return the antecedents and the consequent of a definite clause.""" + assert is_definite_clause(s) + if is_symbol(s.op): + return [], s + else: + antecedent, consequent = s.args + return conjuncts(antecedent), consequent + + +# Useful constant Exprs used in examples and code: +A, B, C, D, E, F, G, P, Q, x, y, z = map(Expr, 'ABCDEFGPQxyz') + + +# ______________________________________________________________________________ +# 7.4.4 A simple inference procedure + + +def tt_entails(kb, alpha): + """ + Does kb entail the sentence alpha? Use truth tables. For propositional + kb's and sentences. [Figure 7.10]. Note that the 'kb' should be an + Expr which is a conjunction of clauses. + >>> tt_entails(expr('P & Q'), expr('Q')) + True + """ + assert not variables(alpha) + symbols = list(prop_symbols(kb & alpha)) + return tt_check_all(kb, alpha, symbols, {}) + + +def tt_check_all(kb, alpha, symbols, model): + """Auxiliary routine to implement tt_entails.""" + if not symbols: + if pl_true(kb, model): + result = pl_true(alpha, model) + assert result in (True, False) + return result + else: + return True + else: + P, rest = symbols[0], symbols[1:] + return (tt_check_all(kb, alpha, rest, extend(model, P, True)) and + tt_check_all(kb, alpha, rest, extend(model, P, False))) + + +def prop_symbols(x): + """Return the set of all propositional symbols in x.""" + if not isinstance(x, Expr): + return set() + elif is_prop_symbol(x.op): + return {x} + else: + return {symbol for arg in x.args for symbol in prop_symbols(arg)} + + +def constant_symbols(x): + """Return the set of all constant symbols in x.""" + if not isinstance(x, Expr): + return set() + elif is_prop_symbol(x.op) and not x.args: + return {x} + else: + return {symbol for arg in x.args for symbol in constant_symbols(arg)} + + +def predicate_symbols(x): + """ + Return a set of (symbol_name, arity) in x. + All symbols (even functional) with arity > 0 are considered. + """ + if not isinstance(x, Expr) or not x.args: + return set() + pred_set = {(x.op, len(x.args))} if is_prop_symbol(x.op) else set() + pred_set.update({symbol for arg in x.args for symbol in predicate_symbols(arg)}) + return pred_set + + +def tt_true(s): + """Is a propositional sentence a tautology? + >>> tt_true('P | ~P') + True + """ + s = expr(s) + return tt_entails(True, s) + + +def pl_true(exp, model={}): + """ + Return True if the propositional logic expression is true in the model, + and False if it is false. If the model does not specify the value for + every proposition, this may return None to indicate 'not obvious'; + this may happen even when the expression is tautological. + >>> pl_true(P, {}) is None + True + """ + if exp in (True, False): + return exp + op, args = exp.op, exp.args + if is_prop_symbol(op): + return model.get(exp) + elif op == '~': + p = pl_true(args[0], model) + if p is None: + return None + else: + return not p + elif op == '|': + result = False + for arg in args: + p = pl_true(arg, model) + if p is True: + return True + if p is None: + result = None + return result + elif op == '&': + result = True + for arg in args: + p = pl_true(arg, model) + if p is False: + return False + if p is None: + result = None + return result + p, q = args + if op == '==>': + return pl_true(~p | q, model) + elif op == '<==': + return pl_true(p | ~q, model) + pt = pl_true(p, model) + if pt is None: + return None + qt = pl_true(q, model) + if qt is None: + return None + if op == '<=>': + return pt == qt + elif op == '^': # xor or 'not equivalent' + return pt != qt + else: + raise ValueError("illegal operator in logic expression" + str(exp)) + + +# ______________________________________________________________________________ +# 7.5 Propositional Theorem Proving + + +def to_cnf(s): + """Convert a propositional logical sentence to conjunctive normal form. + That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 253] + >>> to_cnf('~(B | C)') + (~B & ~C) + """ + s = expr(s) + if isinstance(s, str): + s = expr(s) + s = eliminate_implications(s) # Steps 1, 2 from p. 253 + s = move_not_inwards(s) # Step 3 + return distribute_and_over_or(s) # Step 4 + + +def eliminate_implications(s): + """Change implications into equivalent form with only &, |, and ~ as logical operators.""" + s = expr(s) + if not s.args or is_symbol(s.op): + return s # Atoms are unchanged. + args = list(map(eliminate_implications, s.args)) + a, b = args[0], args[-1] + if s.op == '==>': + return b | ~a + elif s.op == '<==': + return a | ~b + elif s.op == '<=>': + return (a | ~b) & (b | ~a) + elif s.op == '^': + assert len(args) == 2 # TODO: relax this restriction + return (a & ~b) | (~a & b) + else: + assert s.op in ('&', '|', '~') + return Expr(s.op, *args) + + +def move_not_inwards(s): + """Rewrite sentence s by moving negation sign inward. + >>> move_not_inwards(~(A | B)) + (~A & ~B) + """ + s = expr(s) + if s.op == '~': + def NOT(b): + return move_not_inwards(~b) + + a = s.args[0] + if a.op == '~': + return move_not_inwards(a.args[0]) # ~~A ==> A + if a.op == '&': + return associate('|', list(map(NOT, a.args))) + if a.op == '|': + return associate('&', list(map(NOT, a.args))) + return s + elif is_symbol(s.op) or not s.args: + return s + else: + return Expr(s.op, *list(map(move_not_inwards, s.args))) + + +def distribute_and_over_or(s): + """Given a sentence s consisting of conjunctions and disjunctions + of literals, return an equivalent sentence in CNF. + >>> distribute_and_over_or((A & B) | C) + ((A | C) & (B | C)) + """ + s = expr(s) + if s.op == '|': + s = associate('|', s.args) + if s.op != '|': + return distribute_and_over_or(s) + if len(s.args) == 0: + return False + if len(s.args) == 1: + return distribute_and_over_or(s.args[0]) + conj = first(arg for arg in s.args if arg.op == '&') + if not conj: + return s + others = [a for a in s.args if a is not conj] + rest = associate('|', others) + return associate('&', [distribute_and_over_or(c | rest) + for c in conj.args]) + elif s.op == '&': + return associate('&', list(map(distribute_and_over_or, s.args))) + else: + return s + + +def associate(op, args): + """Given an associative op, return an expression with the same + meaning as Expr(op, *args), but flattened -- that is, with nested + instances of the same op promoted to the top level. + >>> associate('&', [(A&B),(B|C),(B&C)]) + (A & B & (B | C) & B & C) + >>> associate('|', [A|(B|(C|(A&B)))]) + (A | B | C | (A & B)) + """ + args = dissociate(op, args) + if len(args) == 0: + return _op_identity[op] + elif len(args) == 1: + return args[0] + else: + return Expr(op, *args) + + +_op_identity = {'&': True, '|': False, '+': 0, '*': 1} + + +def dissociate(op, args): + """Given an associative op, return a flattened list result such + that Expr(op, *result) means the same as Expr(op, *args). + >>> dissociate('&', [A & B]) + [A, B] + """ + result = [] + + def collect(subargs): + for arg in subargs: + if arg.op == op: + collect(arg.args) + else: + result.append(arg) + + collect(args) + return result + + +def conjuncts(s): + """Return a list of the conjuncts in the sentence s. + >>> conjuncts(A & B) + [A, B] + >>> conjuncts(A | B) + [(A | B)] + """ + return dissociate('&', [s]) + + +def disjuncts(s): + """Return a list of the disjuncts in the sentence s. + >>> disjuncts(A | B) + [A, B] + >>> disjuncts(A & B) + [(A & B)] + """ + return dissociate('|', [s]) + + +# ______________________________________________________________________________ + + +def pl_resolution(KB, alpha): + """ + Propositional-logic resolution: say if alpha follows from KB. [Figure 7.12] + >>> pl_resolution(horn_clauses_KB, A) + True + """ + clauses = KB.clauses + conjuncts(to_cnf(~alpha)) + new = set() + while True: + n = len(clauses) + pairs = [(clauses[i], clauses[j]) + for i in range(n) for j in range(i + 1, n)] + for (ci, cj) in pairs: + resolvents = pl_resolve(ci, cj) + if False in resolvents: + return True + new = new.union(set(resolvents)) + if new.issubset(set(clauses)): + return False + for c in new: + if c not in clauses: + clauses.append(c) + + +def pl_resolve(ci, cj): + """Return all clauses that can be obtained by resolving clauses ci and cj.""" + clauses = [] + for di in disjuncts(ci): + for dj in disjuncts(cj): + if di == ~dj or ~di == dj: + dnew = unique(remove_all(di, disjuncts(ci)) + + remove_all(dj, disjuncts(cj))) + clauses.append(associate('|', dnew)) + return clauses + + +# ______________________________________________________________________________ +# 7.5.4 Forward and backward chaining + + +class PropDefiniteKB(PropKB): + """A KB of propositional definite clauses.""" + + def tell(self, sentence): + """Add a definite clause to this KB.""" + assert is_definite_clause(sentence), "Must be definite clause" + self.clauses.append(sentence) + + def ask_generator(self, query): + """Yield the empty substitution if KB implies query; else nothing.""" + if pl_fc_entails(self.clauses, query): + yield {} + + def retract(self, sentence): + self.clauses.remove(sentence) + + def clauses_with_premise(self, p): + """Return a list of the clauses in KB that have p in their premise. + This could be cached away for O(1) speed, but we'll recompute it.""" + return [c for c in self.clauses + if c.op == '==>' and p in conjuncts(c.args[0])] + + +def pl_fc_entails(KB, q): + """Use forward chaining to see if a PropDefiniteKB entails symbol q. + [Figure 7.15] + >>> pl_fc_entails(horn_clauses_KB, expr('Q')) + True + """ + count = {c: len(conjuncts(c.args[0])) + for c in KB.clauses + if c.op == '==>'} + inferred = defaultdict(bool) + agenda = [s for s in KB.clauses if is_prop_symbol(s.op)] + while agenda: + p = agenda.pop() + if p == q: + return True + if not inferred[p]: + inferred[p] = True + for c in KB.clauses_with_premise(p): + count[c] -= 1 + if count[c] == 0: + agenda.append(c.args[1]) + return False + + +""" [Figure 7.13] +Simple inference in a wumpus world example +""" +wumpus_world_inference = expr("(B11 <=> (P12 | P21)) & ~B11") + +""" [Figure 7.16] +Propositional Logic Forward Chaining example +""" +horn_clauses_KB = PropDefiniteKB() +for s in "P==>Q; (L&M)==>P; (B&L)==>M; (A&P)==>L; (A&B)==>L; A;B".split(';'): + horn_clauses_KB.tell(expr(s)) + +""" +Definite clauses KB example +""" +definite_clauses_KB = PropDefiniteKB() +for clause in ['(B & F)==>E', '(A & E & F)==>G', '(B & C)==>F', '(A & B)==>D', '(E & F)==>H', '(H & I)==>J', 'A', 'B', + 'C']: + definite_clauses_KB.tell(expr(clause)) + + +# ______________________________________________________________________________ +# 7.6 Effective Propositional Model Checking +# DPLL-Satisfiable [Figure 7.17] + + +def dpll_satisfiable(s): + """Check satisfiability of a propositional sentence. + This differs from the book code in two ways: (1) it returns a model + rather than True when it succeeds; this is more useful. (2) The + function find_pure_symbol is passed a list of unknown clauses, rather + than a list of all clauses and the model; this is more efficient. + >>> dpll_satisfiable(A |'<=>'| B) == {A: True, B: True} + True + """ + clauses = conjuncts(to_cnf(s)) + symbols = list(prop_symbols(s)) + return dpll(clauses, symbols, {}) + + +def dpll(clauses, symbols, model): + """See if the clauses are true in a partial model.""" + unknown_clauses = [] # clauses with an unknown truth value + for c in clauses: + val = pl_true(c, model) + if val is False: + return False + if val is not True: + unknown_clauses.append(c) + if not unknown_clauses: + return model + P, value = find_pure_symbol(symbols, unknown_clauses) + if P: + return dpll(clauses, remove_all(P, symbols), extend(model, P, value)) + P, value = find_unit_clause(clauses, model) + if P: + return dpll(clauses, remove_all(P, symbols), extend(model, P, value)) + if not symbols: + raise TypeError("Argument should be of the type Expr.") + P, symbols = symbols[0], symbols[1:] + return (dpll(clauses, symbols, extend(model, P, True)) or + dpll(clauses, symbols, extend(model, P, False))) + + +def find_pure_symbol(symbols, clauses): + """ + Find a symbol and its value if it appears only as a positive literal + (or only as a negative) in clauses. + >>> find_pure_symbol([A, B, C], [A|~B,~B|~C,C|A]) + (A, True) + """ + for s in symbols: + found_pos, found_neg = False, False + for c in clauses: + if not found_pos and s in disjuncts(c): + found_pos = True + if not found_neg and ~s in disjuncts(c): + found_neg = True + if found_pos != found_neg: + return s, found_pos + return None, None + + +def find_unit_clause(clauses, model): + """ + Find a forced assignment if possible from a clause with only 1 + variable not bound in the model. + >>> find_unit_clause([A|B|C, B|~C, ~A|~B], {A:True}) + (B, False) + """ + for clause in clauses: + P, value = unit_clause_assign(clause, model) + if P: + return P, value + return None, None + + +def unit_clause_assign(clause, model): + """Return a single variable/value pair that makes clause true in + the model, if possible. + >>> unit_clause_assign(A|B|C, {A:True}) + (None, None) + >>> unit_clause_assign(B|~C, {A:True}) + (None, None) + >>> unit_clause_assign(~A|~B, {A:True}) + (B, False) + """ + P, value = None, None + for literal in disjuncts(clause): + sym, positive = inspect_literal(literal) + if sym in model: + if model[sym] == positive: + return None, None # clause already True + elif P: + return None, None # more than 1 unbound variable + else: + P, value = sym, positive + return P, value + + +def inspect_literal(literal): + """The symbol in this literal, and the value it should take to + make the literal true. + >>> inspect_literal(P) + (P, True) + >>> inspect_literal(~P) + (P, False) + """ + if literal.op == '~': + return literal.args[0], False + else: + return literal, True + + +# ______________________________________________________________________________ +# 7.6.2 Local search algorithms +# Walk-SAT [Figure 7.18] + + +def WalkSAT(clauses, p=0.5, max_flips=10000): + """ + Checks for satisfiability of all clauses by randomly flipping values of variables + >>> WalkSAT([A & ~A], 0.5, 100) is None + True + """ + # Set of all symbols in all clauses + symbols = {sym for clause in clauses for sym in prop_symbols(clause)} + # model is a random assignment of true/false to the symbols in clauses + model = {s: random.choice([True, False]) for s in symbols} + for i in range(max_flips): + satisfied, unsatisfied = [], [] + for clause in clauses: + (satisfied if pl_true(clause, model) else unsatisfied).append(clause) + if not unsatisfied: # if model satisfies all the clauses + return model + clause = random.choice(unsatisfied) + if probability(p): + sym = random.choice(list(prop_symbols(clause))) + else: + # Flip the symbol in clause that maximizes number of sat. clauses + def sat_count(sym): + # Return the the number of clauses satisfied after flipping the symbol. + model[sym] = not model[sym] + count = len([clause for clause in clauses if pl_true(clause, model)]) + model[sym] = not model[sym] + return count + + sym = max(prop_symbols(clause), key=sat_count) + model[sym] = not model[sym] + # If no solution is found within the flip limit, we return failure + return None + + +# ______________________________________________________________________________ +# 7.7 Agents Based on Propositional Logic +# 7.7.1 The current state of the world + + +class WumpusKB(PropKB): + """ + Create a Knowledge Base that contains the atemporal "Wumpus physics" and temporal rules with time zero. + """ + + def __init__(self, dimrow): + super().__init__() + self.dimrow = dimrow + self.tell(~wumpus(1, 1)) + self.tell(~pit(1, 1)) + + for y in range(1, dimrow + 1): + for x in range(1, dimrow + 1): + + pits_in = list() + wumpus_in = list() + + if x > 1: # West room exists + pits_in.append(pit(x - 1, y)) + wumpus_in.append(wumpus(x - 1, y)) + + if y < dimrow: # North room exists + pits_in.append(pit(x, y + 1)) + wumpus_in.append(wumpus(x, y + 1)) + + if x < dimrow: # East room exists + pits_in.append(pit(x + 1, y)) + wumpus_in.append(wumpus(x + 1, y)) + + if y > 1: # South room exists + pits_in.append(pit(x, y - 1)) + wumpus_in.append(wumpus(x, y - 1)) + + self.tell(equiv(breeze(x, y), new_disjunction(pits_in))) + self.tell(equiv(stench(x, y), new_disjunction(wumpus_in))) + + # Rule that describes existence of at least one Wumpus + wumpus_at_least = list() + for x in range(1, dimrow + 1): + for y in range(1, dimrow + 1): + wumpus_at_least.append(wumpus(x, y)) + + self.tell(new_disjunction(wumpus_at_least)) + + # Rule that describes existence of at most one Wumpus + for i in range(1, dimrow + 1): + for j in range(1, dimrow + 1): + for u in range(1, dimrow + 1): + for v in range(1, dimrow + 1): + if i != u or j != v: + self.tell(~wumpus(i, j) | ~wumpus(u, v)) + + # Temporal rules at time zero + self.tell(location(1, 1, 0)) + for i in range(1, dimrow + 1): + for j in range(1, dimrow + 1): + self.tell(implies(location(i, j, 0), equiv(percept_breeze(0), breeze(i, j)))) + self.tell(implies(location(i, j, 0), equiv(percept_stench(0), stench(i, j)))) + if i != 1 or j != 1: + self.tell(~location(i, j, 0)) + + self.tell(wumpus_alive(0)) + self.tell(have_arrow(0)) + self.tell(facing_east(0)) + self.tell(~facing_north(0)) + self.tell(~facing_south(0)) + self.tell(~facing_west(0)) + + def make_action_sentence(self, action, time): + actions = [move_forward(time), shoot(time), turn_left(time), turn_right(time)] + + for a in actions: + if action is a: + self.tell(action) + else: + self.tell(~a) + + def make_percept_sentence(self, percept, time): + # Glitter, Bump, Stench, Breeze, Scream + flags = [0, 0, 0, 0, 0] + + # Things perceived + if isinstance(percept, Glitter): + flags[0] = 1 + self.tell(percept_glitter(time)) + elif isinstance(percept, Bump): + flags[1] = 1 + self.tell(percept_bump(time)) + elif isinstance(percept, Stench): + flags[2] = 1 + self.tell(percept_stench(time)) + elif isinstance(percept, Breeze): + flags[3] = 1 + self.tell(percept_breeze(time)) + elif isinstance(percept, Scream): + flags[4] = 1 + self.tell(percept_scream(time)) + + # Things not perceived + for i in range(len(flags)): + if flags[i] == 0: + if i == 0: + self.tell(~percept_glitter(time)) + elif i == 1: + self.tell(~percept_bump(time)) + elif i == 2: + self.tell(~percept_stench(time)) + elif i == 3: + self.tell(~percept_breeze(time)) + elif i == 4: + self.tell(~percept_scream(time)) + + def add_temporal_sentences(self, time): + if time == 0: + return + t = time - 1 + + # current location rules + for i in range(1, self.dimrow + 1): + for j in range(1, self.dimrow + 1): + self.tell(implies(location(i, j, time), equiv(percept_breeze(time), breeze(i, j)))) + self.tell(implies(location(i, j, time), equiv(percept_stench(time), stench(i, j)))) + + s = list() + + s.append( + equiv( + location(i, j, time), location(i, j, time) & ~move_forward(time) | percept_bump(time))) + + if i != 1: + s.append(location(i - 1, j, t) & facing_east(t) & move_forward(t)) + + if i != self.dimrow: + s.append(location(i + 1, j, t) & facing_west(t) & move_forward(t)) + + if j != 1: + s.append(location(i, j - 1, t) & facing_north(t) & move_forward(t)) + + if j != self.dimrow: + s.append(location(i, j + 1, t) & facing_south(t) & move_forward(t)) + + # add sentence about location i,j + self.tell(new_disjunction(s)) + + # add sentence about safety of location i,j + self.tell( + equiv(ok_to_move(i, j, time), ~pit(i, j) & ~wumpus(i, j) & wumpus_alive(time)) + ) + + # Rules about current orientation + + a = facing_north(t) & turn_right(t) + b = facing_south(t) & turn_left(t) + c = facing_east(t) & ~turn_left(t) & ~turn_right(t) + s = equiv(facing_east(time), a | b | c) + self.tell(s) + + a = facing_north(t) & turn_left(t) + b = facing_south(t) & turn_right(t) + c = facing_west(t) & ~turn_left(t) & ~turn_right(t) + s = equiv(facing_west(time), a | b | c) + self.tell(s) + + a = facing_east(t) & turn_left(t) + b = facing_west(t) & turn_right(t) + c = facing_north(t) & ~turn_left(t) & ~turn_right(t) + s = equiv(facing_north(time), a | b | c) + self.tell(s) + + a = facing_west(t) & turn_left(t) + b = facing_east(t) & turn_right(t) + c = facing_south(t) & ~turn_left(t) & ~turn_right(t) + s = equiv(facing_south(time), a | b | c) + self.tell(s) + + # Rules about last action + self.tell(equiv(move_forward(t), ~turn_right(t) & ~turn_left(t))) + + # Rule about the arrow + self.tell(equiv(have_arrow(time), have_arrow(t) & ~shoot(t))) + + # Rule about Wumpus (dead or alive) + self.tell(equiv(wumpus_alive(time), wumpus_alive(t) & ~percept_scream(time))) + + def ask_if_true(self, query): + return pl_resolution(self, query) + + +# ______________________________________________________________________________ + + +class WumpusPosition: + def __init__(self, x, y, orientation): + self.X = x + self.Y = y + self.orientation = orientation + + def get_location(self): + return self.X, self.Y + + def set_location(self, x, y): + self.X = x + self.Y = y + + def get_orientation(self): + return self.orientation + + def set_orientation(self, orientation): + self.orientation = orientation + + def __eq__(self, other): + if (other.get_location() == self.get_location() and + other.get_orientation() == self.get_orientation()): + return True + else: + return False + + +# ______________________________________________________________________________ +# 7.7.2 A hybrid agent + + +class HybridWumpusAgent(Agent): + """An agent for the wumpus world that does logical inference. [Figure 7.20]""" + + def __init__(self, dimentions): + self.dimrow = dimentions + self.kb = WumpusKB(self.dimrow) + self.t = 0 + self.plan = list() + self.current_position = WumpusPosition(1, 1, 'UP') + super().__init__(self.execute) + + def execute(self, percept): + self.kb.make_percept_sentence(percept, self.t) + self.kb.add_temporal_sentences(self.t) + + temp = list() + + for i in range(1, self.dimrow + 1): + for j in range(1, self.dimrow + 1): + if self.kb.ask_if_true(location(i, j, self.t)): + temp.append(i) + temp.append(j) + + if self.kb.ask_if_true(facing_north(self.t)): + self.current_position = WumpusPosition(temp[0], temp[1], 'UP') + elif self.kb.ask_if_true(facing_south(self.t)): + self.current_position = WumpusPosition(temp[0], temp[1], 'DOWN') + elif self.kb.ask_if_true(facing_west(self.t)): + self.current_position = WumpusPosition(temp[0], temp[1], 'LEFT') + elif self.kb.ask_if_true(facing_east(self.t)): + self.current_position = WumpusPosition(temp[0], temp[1], 'RIGHT') + + safe_points = list() + for i in range(1, self.dimrow + 1): + for j in range(1, self.dimrow + 1): + if self.kb.ask_if_true(ok_to_move(i, j, self.t)): + safe_points.append([i, j]) + + if self.kb.ask_if_true(percept_glitter(self.t)): + goals = list() + goals.append([1, 1]) + self.plan.append('Grab') + actions = self.plan_route(self.current_position, goals, safe_points) + self.plan.extend(actions) + self.plan.append('Climb') + + if len(self.plan) == 0: + unvisited = list() + for i in range(1, self.dimrow + 1): + for j in range(1, self.dimrow + 1): + for k in range(self.t): + if self.kb.ask_if_true(location(i, j, k)): + unvisited.append([i, j]) + unvisited_and_safe = list() + for u in unvisited: + for s in safe_points: + if u not in unvisited_and_safe and s == u: + unvisited_and_safe.append(u) + + temp = self.plan_route(self.current_position, unvisited_and_safe, safe_points) + self.plan.extend(temp) + + if len(self.plan) == 0 and self.kb.ask_if_true(have_arrow(self.t)): + possible_wumpus = list() + for i in range(1, self.dimrow + 1): + for j in range(1, self.dimrow + 1): + if not self.kb.ask_if_true(wumpus(i, j)): + possible_wumpus.append([i, j]) + + temp = self.plan_shot(self.current_position, possible_wumpus, safe_points) + self.plan.extend(temp) + + if len(self.plan) == 0: + not_unsafe = list() + for i in range(1, self.dimrow + 1): + for j in range(1, self.dimrow + 1): + if not self.kb.ask_if_true(ok_to_move(i, j, self.t)): + not_unsafe.append([i, j]) + temp = self.plan_route(self.current_position, not_unsafe, safe_points) + self.plan.extend(temp) + + if len(self.plan) == 0: + start = list() + start.append([1, 1]) + temp = self.plan_route(self.current_position, start, safe_points) + self.plan.extend(temp) + self.plan.append('Climb') + + action = self.plan[0] + self.plan = self.plan[1:] + self.kb.make_action_sentence(action, self.t) + self.t += 1 + + return action + + def plan_route(self, current, goals, allowed): + problem = PlanRoute(current, goals, allowed, self.dimrow) + return astar_search(problem).solution() + + def plan_shot(self, current, goals, allowed): + shooting_positions = set() + + for loc in goals: + x = loc[0] + y = loc[1] + for i in range(1, self.dimrow + 1): + if i < x: + shooting_positions.add(WumpusPosition(i, y, 'EAST')) + if i > x: + shooting_positions.add(WumpusPosition(i, y, 'WEST')) + if i < y: + shooting_positions.add(WumpusPosition(x, i, 'NORTH')) + if i > y: + shooting_positions.add(WumpusPosition(x, i, 'SOUTH')) + + # Can't have a shooting position from any of the rooms the Wumpus could reside + orientations = ['EAST', 'WEST', 'NORTH', 'SOUTH'] + for loc in goals: + for orientation in orientations: + shooting_positions.remove(WumpusPosition(loc[0], loc[1], orientation)) + + actions = list() + actions.extend(self.plan_route(current, shooting_positions, allowed)) + actions.append('Shoot') + return actions + + +# ______________________________________________________________________________ +# 7.7.4 Making plans by propositional inference + + +def SAT_plan(init, transition, goal, t_max, SAT_solver=dpll_satisfiable): + """Converts a planning problem to Satisfaction problem by translating it to a cnf sentence. + [Figure 7.22] + >>> transition = {'A': {'Left': 'A', 'Right': 'B'}, 'B': {'Left': 'A', 'Right': 'C'}, 'C': {'Left': 'B', 'Right': 'C'}} + >>> SAT_plan('A', transition, 'C', 2) is None + True + """ + + # Functions used by SAT_plan + def translate_to_SAT(init, transition, goal, time): + clauses = [] + states = [state for state in transition] + + # Symbol claiming state s at time t + state_counter = itertools.count() + for s in states: + for t in range(time + 1): + state_sym[s, t] = Expr("State_{}".format(next(state_counter))) + + # Add initial state axiom + clauses.append(state_sym[init, 0]) + + # Add goal state axiom + clauses.append(state_sym[goal, time]) + + # All possible transitions + transition_counter = itertools.count() + for s in states: + for action in transition[s]: + s_ = transition[s][action] + for t in range(time): + # Action 'action' taken from state 's' at time 't' to reach 's_' + action_sym[s, action, t] = Expr( + "Transition_{}".format(next(transition_counter))) + + # Change the state from s to s_ + clauses.append(action_sym[s, action, t] | '==>' | state_sym[s, t]) + clauses.append(action_sym[s, action, t] | '==>' | state_sym[s_, t + 1]) + + # Allow only one state at any time + for t in range(time + 1): + # must be a state at any time + clauses.append(associate('|', [state_sym[s, t] for s in states])) + + for s in states: + for s_ in states[states.index(s) + 1:]: + # for each pair of states s, s_ only one is possible at time t + clauses.append((~state_sym[s, t]) | (~state_sym[s_, t])) + + # Restrict to one transition per timestep + for t in range(time): + # list of possible transitions at time t + transitions_t = [tr for tr in action_sym if tr[2] == t] + + # make sure at least one of the transitions happens + clauses.append(associate('|', [action_sym[tr] for tr in transitions_t])) + + for tr in transitions_t: + for tr_ in transitions_t[transitions_t.index(tr) + 1:]: + # there cannot be two transitions tr and tr_ at time t + clauses.append(~action_sym[tr] | ~action_sym[tr_]) + + # Combine the clauses to form the cnf + return associate('&', clauses) + + def extract_solution(model): + true_transitions = [t for t in action_sym if model[action_sym[t]]] + # Sort transitions based on time, which is the 3rd element of the tuple + true_transitions.sort(key=lambda x: x[2]) + return [action for s, action, time in true_transitions] + + # Body of SAT_plan algorithm + for t in range(t_max): + # dictionaries to help extract the solution from model + state_sym = {} + action_sym = {} + + cnf = translate_to_SAT(init, transition, goal, t) + model = SAT_solver(cnf) + if model is not False: + return extract_solution(model) + return None + + +# ______________________________________________________________________________ +# Chapter 9 Inference in First Order Logic +# 9.2 Unification and First Order Inference +# 9.2.1 Unification + + +def unify(x, y, s={}): + """Unify expressions x,y with substitution s; return a substitution that + would make x,y equal, or None if x,y can not unify. x and y can be + variables (e.g. Expr('x')), constants, lists, or Exprs. [Figure 9.1] + >>> unify(x, 3, {}) + {x: 3} + """ + if s is None: + return None + elif x == y: + return s + elif is_variable(x): + return unify_var(x, y, s) + elif is_variable(y): + return unify_var(y, x, s) + elif isinstance(x, Expr) and isinstance(y, Expr): + return unify(x.args, y.args, unify(x.op, y.op, s)) + elif isinstance(x, str) or isinstance(y, str): + return None + elif issequence(x) and issequence(y) and len(x) == len(y): + if not x: + return s + return unify(x[1:], y[1:], unify(x[0], y[0], s)) + else: + return None + + +def is_variable(x): + """A variable is an Expr with no args and a lowercase symbol as the op.""" + return isinstance(x, Expr) and not x.args and x.op[0].islower() + + +def unify_var(var, x, s): + if var in s: + return unify(s[var], x, s) + elif x in s: + return unify(var, s[x], s) + elif occur_check(var, x, s): + return None + else: + return extend(s, var, x) + + +def occur_check(var, x, s): + """Return true if variable var occurs anywhere in x + (or in subst(s, x), if s has a binding for x).""" + if var == x: + return True + elif is_variable(x) and x in s: + return occur_check(var, s[x], s) + elif isinstance(x, Expr): + return (occur_check(var, x.op, s) or + occur_check(var, x.args, s)) + elif isinstance(x, (list, tuple)): + return first(e for e in x if occur_check(var, e, s)) + else: + return False + + +def extend(s, var, val): + """Copy the substitution s and extend it by setting var to val; return copy. + >>> extend({x: 1}, y, 2) == {x: 1, y: 2} + True + """ + s2 = s.copy() + s2[var] = val + return s2 + + +# 9.2.2 Storage and retrieval + + +class FolKB(KB): + """A knowledge base consisting of first-order definite clauses. + >>> kb0 = FolKB([expr('Farmer(Mac)'), expr('Rabbit(Pete)'), + ... expr('(Rabbit(r) & Farmer(f)) ==> Hates(f, r)')]) + >>> kb0.tell(expr('Rabbit(Flopsie)')) + >>> kb0.retract(expr('Rabbit(Pete)')) + >>> kb0.ask(expr('Hates(Mac, x)'))[x] + Flopsie + >>> kb0.ask(expr('Wife(Pete, x)')) + False + """ + + def __init__(self, initial_clauses=None): + self.clauses = [] # inefficient: no indexing + if initial_clauses: + for clause in initial_clauses: + self.tell(clause) + + def tell(self, sentence): + if is_definite_clause(sentence): + self.clauses.append(sentence) + else: + raise Exception("Not a definite clause: {}".format(sentence)) + + def ask_generator(self, query): + return fol_bc_ask(self, query) + + def retract(self, sentence): + self.clauses.remove(sentence) + + def fetch_rules_for_goal(self, goal): + return self.clauses + + +# ______________________________________________________________________________ +# 9.3 Forward Chaining +# 9.3.2 A simple forward-chaining algorithm + + +def fol_fc_ask(KB, alpha): + """A simple forward-chaining algorithm. [Figure 9.3]""" + kb_consts = list({c for clause in KB.clauses for c in constant_symbols(clause)}) + + def enum_subst(p): + query_vars = list({v for clause in p for v in variables(clause)}) + for assignment_list in itertools.product(kb_consts, repeat=len(query_vars)): + theta = {x: y for x, y in zip(query_vars, assignment_list)} + yield theta + + # check if we can answer without new inferences + for q in KB.clauses: + phi = unify(q, alpha, {}) + if phi is not None: + yield phi + + while True: + new = [] + for rule in KB.clauses: + p, q = parse_definite_clause(rule) + for theta in enum_subst(p): + if set(subst(theta, p)).issubset(set(KB.clauses)): + q_ = subst(theta, q) + if all([unify(x, q_, {}) is None for x in KB.clauses + new]): + new.append(q_) + phi = unify(q_, alpha, {}) + if phi is not None: + yield phi + if not new: + break + for clause in new: + KB.tell(clause) + return None + + +def subst(s, x): + """Substitute the substitution s into the expression x. + >>> subst({x: 42, y:0}, F(x) + y) + (F(42) + 0) + """ + if isinstance(x, list): + return [subst(s, xi) for xi in x] + elif isinstance(x, tuple): + return tuple([subst(s, xi) for xi in x]) + elif not isinstance(x, Expr): + return x + elif is_var_symbol(x.op): + return s.get(x, x) + else: + return Expr(x.op, *[subst(s, arg) for arg in x.args]) + + +def standardize_variables(sentence, dic=None): + """Replace all the variables in sentence with new variables.""" + if dic is None: + dic = {} + if not isinstance(sentence, Expr): + return sentence + elif is_var_symbol(sentence.op): + if sentence in dic: + return dic[sentence] + else: + v = Expr('v_{}'.format(next(standardize_variables.counter))) + dic[sentence] = v + return v + else: + return Expr(sentence.op, + *[standardize_variables(a, dic) for a in sentence.args]) + + +standardize_variables.counter = itertools.count() + + +# __________________________________________________________________ +# 9.4 Backward Chaining + + +def fol_bc_ask(KB, query): + """A simple backward-chaining algorithm for first-order logic. [Figure 9.6] + KB should be an instance of FolKB, and query an atomic sentence.""" + return fol_bc_or(KB, query, {}) + + +def fol_bc_or(KB, goal, theta): + for rule in KB.fetch_rules_for_goal(goal): + lhs, rhs = parse_definite_clause(standardize_variables(rule)) + for theta1 in fol_bc_and(KB, lhs, unify(rhs, goal, theta)): + yield theta1 + + +def fol_bc_and(KB, goals, theta): + if theta is None: + pass + elif not goals: + yield theta + else: + first, rest = goals[0], goals[1:] + for theta1 in fol_bc_or(KB, subst(theta, first), theta): + for theta2 in fol_bc_and(KB, rest, theta1): + yield theta2 + + +# ______________________________________________________________________________ +# A simple KB that defines the relevant conditions of the Wumpus World as in Fig 7.4. +# See Sec. 7.4.3 + + +#print ("Testing Wumpus") +#P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21') +#Public prositions +#wumpus_kb.tell(~P11) +#wumpus_kb.tell(B11 | '<=>' | (P12 | P21)) +#wumpus_kb.tell(B21 | '<=>' | (P11 | P22 | P31)) + +#propositions by rminalr + +#wumpus_kb.tell(~B11) +#wumpus_kb.tell(B21) + +#print(to_cnf('~(P11 <=> P12)')) + + + + +test_kb = FolKB( + map(expr, ['Farmer(Mac)', + 'Rabbit(Pete)', + 'Mother(MrsMac, Mac)', + 'Mother(MrsRabbit, Pete)', + '(Rabbit(r) & Farmer(f)) ==> Hates(f, r)', + '(Mother(m, c)) ==> Loves(m, c)', + '(Mother(m, r) & Rabbit(r)) ==> Rabbit(m)', + '(Farmer(f)) ==> Human(f)', + # Note that this order of conjuncts + # would result in infinite recursion: + # '(Human(h) & Mother(m, h)) ==> Human(m)' + '(Mother(m, h) & Human(h)) ==> Human(m)'])) + +crime_kb = FolKB( + map(expr, ['(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)', + 'Owns(Nono, M1)', + 'Missile(M1)', + '(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)', + 'Missile(x) ==> Weapon(x)', + 'Enemy(x, America) ==> Hostile(x)', + 'American(West)', + 'Enemy(Nono, America)'])) + + +# ______________________________________________________________________________ + +# Example application (not in the book). +# You can use the Expr class to do symbolic differentiation. This used to be +# a part of AI; now it is considered a separate field, Symbolic Algebra. + + +def diff(y, x): + """Return the symbolic derivative, dy/dx, as an Expr. + However, you probably want to simplify the results with simp. + >>> diff(x * x, x) + ((x * 1) + (x * 1)) + """ + if y == x: + return 1 + elif not y.args: + return 0 + else: + u, op, v = y.args[0], y.op, y.args[-1] + if op == '+': + return diff(u, x) + diff(v, x) + elif op == '-' and len(y.args) == 1: + return -diff(u, x) + elif op == '-': + return diff(u, x) - diff(v, x) + elif op == '*': + return u * diff(v, x) + v * diff(u, x) + elif op == '/': + return (v * diff(u, x) - u * diff(v, x)) / (v * v) + elif op == '**' and isnumber(x.op): + return (v * u ** (v - 1) * diff(u, x)) + elif op == '**': + return (v * u ** (v - 1) * diff(u, x) + + u ** v * Expr('log')(u) * diff(v, x)) + elif op == 'log': + return diff(u, x) / u + else: + raise ValueError("Unknown op: {} in diff({}, {})".format(op, y, x)) + + +def simp(x): + """Simplify the expression x.""" + if isnumber(x) or not x.args: + return x + args = list(map(simp, x.args)) + u, op, v = args[0], x.op, args[-1] + if op == '+': + if v == 0: + return u + if u == 0: + return v + if u == v: + return 2 * u + if u == -v or v == -u: + return 0 + elif op == '-' and len(args) == 1: + if u.op == '-' and len(u.args) == 1: + return u.args[0] # --y ==> y + elif op == '-': + if v == 0: + return u + if u == 0: + return -v + if u == v: + return 0 + if u == -v or v == -u: + return 0 + elif op == '*': + if u == 0 or v == 0: + return 0 + if u == 1: + return v + if v == 1: + return u + if u == v: + return u ** 2 + elif op == '/': + if u == 0: + return 0 + if v == 0: + return Expr('Undefined') + if u == v: + return 1 + if u == -v or v == -u: + return 0 + elif op == '**': + if u == 0: + return 0 + if v == 0: + return 1 + if u == 1: + return 1 + if v == 1: + return u + elif op == 'log': + if u == 1: + return 0 + else: + raise ValueError("Unknown op: " + op) + # If we fall through to here, we can not simplify further + return Expr(op, *args) + + +def d(y, x): + """Differentiate and then simplify. + >>> d(x * x - x, x) + ((2 * x) - 1) + """ + return simp(diff(y, x)) + +############# +#Testing + +#def main(): +# print ("Hello") + +######## +#Start from Here +#modifications from leonardo bobadilla + + + +''' +#testing Hybrid humpus + + +hybrid_wumpus = HybridWumpusAgent(4) +print("Testing Hybrid Wumpus") + +print(hybrid_wumpus) +print(hybrid_wumpus.kb) + +print(hybrid_wumpus.kb.ask_if_true(wumpus_alive(0))) +print(hybrid_wumpus.kb.ask_if_true((have_arrow(0)))) +print(hybrid_wumpus.kb.ask_if_true((facing_east(0)))) +#print(hybrid_wumpus.kb.ask_if_true((facing_west(0)))) + + +hybrid_wumpus.execute(Stench) + +# self.tell() +#self.tell(have_arrow(0)) +#self.tell(facing_east(0)) +#self.tell(~facing_north(0)) +#self.tell(~facing_south(0)) +#self.tell(~facing_west(0)) + + +#old testing + +wumpus_kb = PropKB() + + + +#print ("Hello, testing code") + +#print ("Hello, testing code") + +#print( "Privacy preserving Wumpus") + +P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21') + + +#Public prositions \alpha_public + +wumpus_kb.tell(~P11) +wumpus_kb.tell(B11 | '<=>' | (P12 | P21)) +wumpus_kb.tell(B21 | '<=>' | (P11 | P22 | P31)) + +#propositions by \alpha_1 + +wumpus_kb.tell(~B11) + +#propositions by \alpha_2 + +wumpus_kb.tell(B21) + +#propositions by \beta + +print(wumpus_kb.ask(~B11)) + + +#TODO: figure out how ask works + +print("cnf conversion") + +#Use DPLL + +print(to_cnf('~(P11 <=> P12)')) + +s = to_cnf('~(P11 <=> P12)') + +s_1 = to_cnf('~P11') +print(s_1) + +#(B11 | '<=>' | (P12 | P21)) +s_2 = to_cnf('(B11 <=> (P12 | P21))') +print(s_2) + + + + +print("concatenation") + + + +#(B21 | '<=>' | (P11 | P22 | P31)) +s_3 = to_cnf('(B21 <=> ((P11 | P22 | P31)))') +print(s_3) + +alpha_public = to_cnf('(~P11 & (B11 <=> (P12 | P21)) & (B21 <=> ((P11 | P22 | P31))) )') +print(alpha_public) + + + +#s_4 = ~B11 +s_4 = to_cnf('~B11') +print(s_4) + + +s_5 = to_cnf('B21') +print(s_5) + + + + + + + + + + +s_6 = to_cnf('~P12') +print(s_6) + + +#TODO: + + +#alpha_pub = +alpha_1 = s_5 +alpha_2 = s_6 +beta = s_6 + + +#I just need to change dpll_ + +alpha_combined = to_cnf('(~P11 & (B11 <=> (P12 | P21)) & (B21 <=> ((P11 | P22 | P31))) & ~B11 & B21 & P12)') +#I just need to change to +result = dpll_satisfiable(alpha_combined) +print(result) + +#dpll_satisfiable(A |'<=>'| B) == {A: True, B: True} + + +#print(s) +#TODO: +#1) Integrate it with the ppSAT +#2) Look at 7.7 see we can use this in to a hybrid agent + + + +print("First Order Logic Example 1") + + +kb0 = FolKB([expr('Farmer(Mac)'), expr('Rabbit(Pete)'), expr('(Rabbit(r) & Farmer(f)) ==> Hates(f, r)')]) +kb0.tell(expr('Rabbit(Flopsie)')) +#kb0.retract(expr('Rabbit(Pete)')) +print(kb0.ask(expr('Hates(Mac, x)'))[x]) +#kb0.ask(expr('Wife(Pete, x)')) + + +print("First Order Logic Example 2") + + +crime_kb = FolKB( + map(expr, ['(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)', + 'Owns(Nono, M1)', + 'Missile(M1)', + '(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)', + 'Missile(x) ==> Weapon(x)', + 'Enemy(x, America) ==> Hostile(x)', + 'American(West)', + 'Enemy(Nono, America)'])) + + + +print(crime_kb) + +print(crime_kb.ask(expr('Criminal(West)'))) + +print(crime_kb.ask(expr('Criminal(x)'))[x]) + + + +print("Print all the clauses") + +for element in crime_kb.clauses: + print(element) + +kb_consts = list({c for clause in crime_kb.clauses for c in constant_symbols(clause)}) +#query_vars = list({v for clause in p for v in variables(clause)}) + +print(kb_consts) +#print(query_vars) + + + +family_kb = FolKB( + map(expr, ['(King(x) & Greedy(x)) ==> Evil(x)', + 'King(John)', + 'Greedy(John)', + 'Brother(Richard, John)'])) + + +print(family_kb.ask(expr('Evil(x)'))[x]) + +#print("Print all the clauses") + + +expression_list = [] +variable = "x" + + +#Add sentences that do not have variables, still hard coded + +for element in family_kb.clauses: + expression = str(element) + if variable not in expression: + print(element) + expression_list.append(expression) + + + +#find ground symbols + +kb_consts = list({c for clause in family_kb.clauses for c in constant_symbols(clause)}) +print(kb_consts) + + +#substituting ground terms in clasuse with variables, this is hard coded still + +for c in kb_consts: + + symbol = str(c) + txt = str(family_kb.clauses[0]) + print (c) + print (family_kb.clauses[0]) + + x = txt.replace("x", symbol) + + print (x) + expression_list.append(x) + + +print("Expresion List") +print(expression_list) + + + +#TEST +#alpha_combined = to_cnf('King(John) & Greedy(John) & Brother(Richard, John) & ( (King(Richard) & Greedy(Richard)) ==> Evil(Richard))') +#print(alpha_combined) +#result = dpll_satisfiable(alpha_combined) +#print(result) + + +#['King(John)', 'Greedy(John)', 'Brother(Richard, John)', '((King(Richard) & Greedy(Richard)) ==> Evil(Richard))', '((King(John) & Greedy(John)) ==> Evil(John))']) +#alpha_combined = to_cnf('(~P11 & (B11 <=> (P12 | P21)) & (B21 <=> ((P11 | P22 | P31))) & ~B11 & B21 & P12)') + + + + + +#join all expressions with & + +result2 = " & ".join(expression_list) + +print(result2) + + +alpha_combined2 = to_cnf(result2) + +result3 = dpll_satisfiable(alpha_combined2) + +print(result3) + + +#See if we can infer Evil(John) + +result4 = result2 +" & "+ "~Evil(John)" +print(result4) + +alpha_combined3 = to_cnf(result4) + + +result5 = dpll_satisfiable(alpha_combined3) + +print(result5) + + +''' + diff --git a/ppsat.py b/ppsat.py new file mode 100644 index 000000000..4d0d486fe --- /dev/null +++ b/ppsat.py @@ -0,0 +1,155 @@ + +from logic4e_modify_v01 import * + +## Alices pass her public to first and Bob passer her public info to second +'''takes thea cnf and converts to form ppsat can understand''' +def cnf_to_ppsat(clause): + clause = str(clause).replace(' | ', " ").replace('~','-') + clauses = clause.split(' & ') + clauses = [("(" + c if c[0] != '(' else c) for c in clauses] + clauses = [ (c + ")" if c[-1] != ')' else c).replace('((','(').replace('))',')') for c in clauses ] + return '"' + " ".join(clauses).strip() + '"' + +def ppsat_to_cnf(clause : str): + ''' + passed in the form {A B C D} + ''' + if not clause: + return None + clause = clause[1:-1] + clause = clause.replace(" ", " & ") + return to_cnf(clause) + + + pass + +class AgentKB(KB): + def __init__(self, master: KB, sentence=None, mode=0): + self.public = [] + self.private = [] + if sentence: + self.tell_public(sentence) if mode == 0 else self.tell_private(sentence) + + ''' + tell accepts a sentence and a mode, if mode is 0 then the sentence is added to public knowledge base + if mode is 1 then the sentence is added to private knowledge base + ''' + def tell(self, sentence, mode = 0): + """Add the sentence to the KB.""" + if mode == 0: + self.tell_public(sentence) + else: + self.tell_private(sentence) + def tell_private(self, sentence): + self.private.extend(conjuncts(to_cnf(sentence))) + def tell_public(self, sentence): + self.public.extend(conjuncts(to_cnf(sentence))) + + def ask_master(self, query): + """Return True if the KB entails query, else return False.""" + return self.ask_if_true(query) + + def ask_generator(self, query): + """Yield the empty substitution {} if KB entails query; else no results.""" + clauses = self.public + self.private + if tt_entails(Expr('&', *clauses), query): + yield {} + + def ask_if_true(self, query): + """Return True if the KB entails query, else return False.""" + for _ in self.ask_generator(query): + return True + return False + + def retract(self, sentence): + """Remove the sentence's clauses from the KB.""" + for c in conjuncts(to_cnf(sentence)): + if c in self.public: + self.clauses.remove(c) + if c in self.private: + self.clauses.remove(c) + ## in order to use share we need both KB parties to be sitting in serber, the calling kb will be Alice and the other will be Bob + + + + + +def ppsat_to_cnf_test(): + t1 = ppsat_to_cnf('{A B C D}') + print("Test 1: {A B C D} -->", t1) + + t2 = ppsat_to_cnf("{A}") + print("Test 2: {A} -->", t2) + + + +def cnf_tests(): + + # Test 1: Biconditional negation conversion using '<=>' + t1 = to_cnf('~(P11 <=> P12)') + print(type(t1)) + print("Test 1: ~(P11 <=> P12) -->", t1) + print("Formatted:", cnf_to_ppsat(t1)) + + # Test 2: Forward implication conversion using '==>' + # Expected conversion: A ==> B becomes B | ~A + t2 = to_cnf('A ==> B') + print("Test 2: A ==> B -->", t2) + print("Formatted:", cnf_to_ppsat(t2)) + + # Test 3: Reverse implication conversion using '<==' + # Expected conversion: A <== B becomes A | ~B + t3 = to_cnf('A <== B') + print("Test 3: A <== B -->", t3) + print("Formatted:", cnf_to_ppsat(t3)) + + # Test 4: Biconditional conversion using '<=>' + # Expected conversion: A <=> B becomes (A | ~B) & (B | ~A) + t4 = to_cnf('A <=> B') + print("Test 4: A <=> B -->", t4) + print("Formatted:", cnf_to_ppsat(t4)) + + # Test 5: Exclusive OR conversion using '^' + # Expected conversion: A ^ B becomes (A & ~B) | (~A & B) + t5 = to_cnf('A ^ B') + print("Test 5: A ^ B -->", t5) + print("Formatted:", cnf_to_ppsat(t5)) + + # Test 6: Standard logical operators + # Example: ~(A | B) should convert to ~A & ~B using De Morgan's law. + t6 = to_cnf('~(A | B)') + print("Test 6: ~(A | B) -->", t6) + print("Formatted:", cnf_to_ppsat(t6)) + + # Test 7: A more complex expression combining various operators + t7 = to_cnf('(A ==> B) & ~(C <=> D) | (E ^ F)') + print("Test 7: (A ==> B) & ~(C <=> D) | (E ^ F) -->", t7) + print("Formatted:", cnf_to_ppsat(t7)) + + # Test 8: Expression already in CNF should remain unchanged. + t8 = to_cnf('(A | ~B) & (C | D)') + print("Test 8: (A | ~B) & (C | D) -->", t8) + print("Formatted:", cnf_to_ppsat(t8)) + + # Test 9: Extra parentheses and whitespace. + t9 = to_cnf(' ((A)) & ( ~(B | C) ) ') + print("Test 9: ((A)) & ( ~(B | C) ) -->", t9) + print("Formatted:", cnf_to_ppsat(t9)) + + # Test 10: Nested implications. + t10 = to_cnf('A ==> (B ==> C)') + print("Test 10: A ==> (B ==> C) -->", t10) + print("Formatted:", cnf_to_ppsat(t10)) + + # Test 11: Single literal (if allowed by your parser). + # If your parser accepts a single literal as a valid expression. + t11 = to_cnf('A') + print("Test 11: A -->", t11) + print("Formatted:", cnf_to_ppsat(t11)) + + + pass + +#cnf_tests() +ppsat_to_cnf_test() + \ No newline at end of file From b4c315e51716e33c5ba096f8d8487c37ce6a29c2 Mon Sep 17 00:00:00 2001 From: Joshua Mayhugh <123776276+jmayhugh1@users.noreply.github.com> Date: Mon, 17 Feb 2025 20:02:36 -0600 Subject: [PATCH 2/3] first commit --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 17f1d6085..5745403c3 100644 --- a/README.md +++ b/README.md @@ -205,3 +205,4 @@ Many thanks for contributions over the years. I got bug reports, corrected code, [search]:../master/search.py [utils]:../master/utils.py [text]:../master/text.py +# DAIR From a407daf56dbbed9aea9fe2a271f8673e958b9f5f Mon Sep 17 00:00:00 2001 From: Joshua Mayhugh <123776276+jmayhugh1@users.noreply.github.com> Date: Mon, 17 Feb 2025 20:18:41 -0600 Subject: [PATCH 3/3] more ppsat --- ppsat.py | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/ppsat.py b/ppsat.py index 4d0d486fe..24c216ce0 100644 --- a/ppsat.py +++ b/ppsat.py @@ -23,10 +23,14 @@ def ppsat_to_cnf(clause : str): pass +def ppsat_wrappet(master, agent): + ## run the ./ppsat with args for + pass class AgentKB(KB): def __init__(self, master: KB, sentence=None, mode=0): self.public = [] self.private = [] + self.master = master if sentence: self.tell_public(sentence) if mode == 0 else self.tell_private(sentence) @@ -45,9 +49,30 @@ def tell_private(self, sentence): def tell_public(self, sentence): self.public.extend(conjuncts(to_cnf(sentence))) - def ask_master(self, query): + def ask_master(self): """Return True if the KB entails query, else return False.""" - return self.ask_if_true(query) + return self.ask_master(self.master) + def _ask_master(self, master): + ## create a connection with + agent_clauses = "" + master_clauses = "" + for c in self.public: + agent_clauses += cnf_to_ppsat(c) + " " + for c in self.private: + agent_clauses += cnf_to_ppsat(c) + " " + for c in master.public: + master_clauses += cnf_to_ppsat(c) + " " + for c in master.private: + master_clauses += cnf_to_ppsat(c) + " " + print("self clauses:", agent_clauses) + print("master clauses:", master_clauses) + ## now go up a file and + + + + + + def ask_generator(self, query): """Yield the empty substitution {} if KB entails query; else no results."""