Logic & Knowledge

Representations and Inference for Logic. (Chapters 7-9, 12)

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 parens 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

class logic.KB(sentence=None)

Bases: object

A knowledge base to which you can tell and ask sentences. To create a KB, first subclass this class and implement tell, ask_generator, and retract. Why ask_generator instead of ask? The book is a bit vague on what ask means – 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.

tell(sentence)

Add the sentence to the KB.

ask(query)

Return a substitution that makes the query true, or, failing that, return False.

ask_generator(query)

Yield all the substitutions that make query true.

retract(sentence)

Remove sentence from the KB.

class logic.PropKB(sentence=None)

Bases: KB

A KB for propositional logic. Inefficient, with no indexing.

tell(sentence)

Add the sentence’s clauses to the KB.

ask_generator(query)

Yield the empty substitution {} if KB entails query; else no results.

ask_if_true(query)

Return True if the KB entails query, else return False.

retract(sentence)

Remove the sentence’s clauses from the KB.

logic.KBAgentProgram(kb)

[Figure 7.1] A generic logical knowledge-based agent program.

logic.is_symbol(s)

A string s is a symbol if it starts with an alphabetic char. >>> is_symbol(‘R2D2’) True

logic.is_var_symbol(s)

A logic variable symbol is an initial-lowercase string. >>> is_var_symbol(‘EXE’) False

logic.is_prop_symbol(s)

A proposition logic symbol is an initial-uppercase string. >>> is_prop_symbol(‘exe’) False

logic.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

logic.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

logic.parse_definite_clause(s)

Return the antecedents and the consequent of a definite clause.

logic.tt_entails(kb, alpha)

[Figure 7.10] Does kb entail the sentence alpha? Use truth tables. For propositional kb’s and sentences. Note that the ‘kb’ should be an Expr which is a conjunction of clauses. >>> tt_entails(expr(‘P & Q’), expr(‘Q’)) True

logic.tt_check_all(kb, alpha, symbols, model)

Auxiliary routine to implement tt_entails.

logic.prop_symbols(x)

Return the set of all propositional symbols in x.

logic.constant_symbols(x)

Return the set of all constant symbols in x.

logic.predicate_symbols(x)

Return a set of (symbol_name, arity) in x. All symbols (even functional) with arity > 0 are considered.

logic.tt_true(s)

Is a propositional sentence a tautology? >>> tt_true(‘P | ~P’) True

logic.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

logic.to_cnf(s)

[Page 253] Convert a propositional logical sentence to conjunctive normal form. That is, to the form ((A | ~B | …) & (B | C | …) & …) >>> to_cnf(‘~(B | C)’) (~B & ~C)

logic.eliminate_implications(s)

Change implications into equivalent form with only &, |, and ~ as logical operators.

logic.move_not_inwards(s)

Rewrite sentence s by moving negation sign inward. >>> move_not_inwards(~(A | B)) (~A & ~B)

logic.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))

logic.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))

logic.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]

logic.conjuncts(s)

Return a list of the conjuncts in the sentence s. >>> conjuncts(A & B) [A, B] >>> conjuncts(A | B) [(A | B)]

logic.disjuncts(s)

Return a list of the disjuncts in the sentence s. >>> disjuncts(A | B) [A, B] >>> disjuncts(A & B) [(A & B)]

logic.pl_resolution(kb, alpha)

[Figure 7.12] Propositional-logic resolution: say if alpha follows from KB. >>> pl_resolution(horn_clauses_KB, A) True

logic.pl_resolve(ci, cj)

Return all clauses that can be obtained by resolving clauses ci and cj.

class logic.PropDefiniteKB(sentence=None)

Bases: PropKB

A KB of propositional definite clauses.

tell(sentence)

Add a definite clause to this KB.

ask_generator(query)

Yield the empty substitution if KB implies query; else nothing.

retract(sentence)

Remove the given definite clause from this KB.

clauses_with_premise(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.

logic.pl_fc_entails(kb, q)

[Figure 7.15] Use forward chaining to see if a PropDefiniteKB entails symbol q. >>> pl_fc_entails(horn_clauses_KB, expr(‘Q’)) True

logic.wumpus_world_inference = ((B11 <=> (P12 | P21)) & ~B11)

[Figure 7.16] Propositional Logic Forward Chaining example

logic.no_branching_heuristic(symbols, clauses)

Default DPLL branching rule: pick the first remaining symbol and try True.

logic.min_clauses(clauses)

Return the clauses of minimum size (treating units as size 2 for MOMS-style heuristics).

logic.moms(symbols, clauses)

MOMS (Maximum Occurrence in clauses of Minimum Size) heuristic Returns the literal with the most occurrences in all clauses of minimum size

logic.momsf(symbols, clauses, k=0)

MOMS alternative heuristic If f(x) the number of occurrences of the variable x in clauses with minimum size, we choose the variable maximizing [f(x) + f(-x)] * 2^k + f(x) * f(-x) Returns x if f(x) >= f(-x) otherwise -x

logic.posit(symbols, clauses)

Freeman’s POSIT version of MOMs Counts the positive x and negative x for each variable x in clauses with minimum size Returns x if f(x) >= f(-x) otherwise -x

logic.zm(symbols, clauses)

Zabih and McAllester’s version of MOMs Counts the negative occurrences only of each variable x in clauses with minimum size

logic.dlis(symbols, clauses)

DLIS (Dynamic Largest Individual Sum) heuristic Choose the variable and value that satisfies the maximum number of unsatisfied clauses Like DLCS but we only consider the literal (thus Cp and Cn are individual)

logic.dlcs(symbols, clauses)

DLCS (Dynamic Largest Combined Sum) heuristic Cp the number of clauses containing literal x Cn the number of clauses containing literal -x Here we select the variable maximizing Cp + Cn Returns x if Cp >= Cn otherwise -x

logic.jw(symbols, clauses)

Jeroslow-Wang heuristic For each literal compute J(l) = sum{l in clause c} 2^{-|c|} Return the literal maximizing J

logic.jw2(symbols, clauses)

Two Sided Jeroslow-Wang heuristic Compute J(l) also counts the negation of l = J(x) + J(-x) Returns x if J(x) >= J(-x) otherwise -x

logic.dpll_satisfiable(s, branching_heuristic=<function no_branching_heuristic>)

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

logic.dpll(clauses, symbols, model, branching_heuristic=<function no_branching_heuristic>)

See if the clauses are true in a partial model.

logic.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)

logic.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)

logic.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)

logic.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)

logic.no_restart(conflicts, restarts, queue_lbd, sum_lbd)

Default CDCL restart policy: never restart.

logic.luby(conflicts, restarts, queue_lbd, sum_lbd, unit=512)

Restart policy based on the Luby sequence (restart after unit * luby(restarts) conflicts).

logic.glucose(conflicts, restarts, queue_lbd, sum_lbd, x=100, k=0.7)

Glucose-style restart policy based on recent vs. global average literal block distance (LBD).

logic.cdcl_satisfiable(s, vsids_decay=0.95, restart_strategy=<function no_restart>)

>>> cdcl_satisfiable(A |'<=>'| B) == {A: True, B: True}
True

logic.assign_decision_literal(symbols, model, scores, G, dl)

Pick the unassigned symbol with the highest VSIDS score, assign it at decision level dl, and record it as a decision node in the implication graph G.

logic.unit_propagation(clauses, symbols, model, G, dl)

Boolean constraint propagation over the two-watched-literal database.

Repeatedly assigns forced literals from unit clauses (extending model and the implication graph G) until a fixpoint is reached. Returns True if a conflict clause is found, else False.

logic.conflict_analysis(G, dl)

Analyse a conflict in the implication graph G using the first-UIP scheme.

Resolves the conflict clause back to the first unique implication point and returns a tuple (backjump_level, learnt_clause, lbd) where lbd is the learnt clause’s literal block distance.

logic.pl_binary_resolution(ci, cj)

Resolve two clauses on a complementary pair of literals and return the resolvent.

logic.backjump(symbols, model, G, dl=0)

Undo all assignments made above decision level dl, restoring those symbols as unassigned.

class logic.TwoWLClauseDatabase(clauses)

Bases: object

Clause database using the two-watched-literal lazy data structure for fast unit propagation.

Maintains, for each clause, two watched literals and, for each literal, the set of clauses in which it is watched (split into positive and negative occurrences).

get_clauses()

Return a view of all clauses currently stored in the database.

set_first_watched(clause, new_watching)

Set the first watched literal of clause (no-op for clauses of length <= 2).

set_second_watched(clause, new_watching)

Set the second watched literal of clause (no-op for clauses of length <= 2).

get_first_watched(clause)

Return the first watched literal of clause.

get_second_watched(clause)

Return the second watched literal of clause.

get_pos_watched(l)

Return the set of clauses in which symbol l is watched positively.

get_neg_watched(l)

Return the set of clauses in which symbol l is watched negatively.

add(clause, model)

Add clause to the database, choosing its two watched literals given model.

remove(clause)

Remove clause from the database and from its watched literals’ watch lists.

update_first_watched(clause, model)

Try to replace the first watched literal of clause with another non-falsified literal.

Returns True if a new watch was installed, otherwise None (the clause stays as is).

update_second_watched(clause, model)

Try to replace the second watched literal of clause with another non-falsified literal.

Returns True if a new watch was installed, otherwise None (the clause stays as is).

logic.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

logic.MapColoringSAT(colors, neighbors)

Make a SAT for the problem of coloring a map with different colors for any two adjacent regions. Arguments are a list of colors, and a dict of {region: [neighbor,…]} entries. This dict may also be specified as a string of the form defined by parse_neighbors.

logic.facing_east(time)

Proposition: the agent is facing east at the given time step.

logic.facing_west(time)

Proposition: the agent is facing west at the given time step.

logic.facing_north(time)

Proposition: the agent is facing north at the given time step.

logic.facing_south(time)

Proposition: the agent is facing south at the given time step.

logic.wumpus(x, y)

Proposition: there is a wumpus in square (x, y).

logic.pit(x, y)

Proposition: there is a pit in square (x, y).

logic.breeze(x, y)

Proposition: there is a breeze in square (x, y).

logic.stench(x, y)

Proposition: there is a stench in square (x, y).

logic.wumpus_alive(time)

Proposition: the wumpus is alive at the given time step.

logic.have_arrow(time)

Proposition: the agent still has its arrow at the given time step.

logic.percept_stench(time)

Proposition: the agent perceives a stench at the given time step.

logic.percept_breeze(time)

Proposition: the agent perceives a breeze at the given time step.

logic.percept_glitter(time)

Proposition: the agent perceives glitter at the given time step.

logic.percept_bump(time)

Proposition: the agent perceives a bump at the given time step.

logic.percept_scream(time)

Proposition: the agent perceives a scream at the given time step.

logic.move_forward(time)

Action proposition: the agent moves forward at the given time step.

logic.shoot(time)

Action proposition: the agent shoots its arrow at the given time step.

logic.turn_left(time)

Action proposition: the agent turns left at the given time step.

logic.turn_right(time)

Action proposition: the agent turns right at the given time step.

logic.ok_to_move(x, y, time)

Proposition: square (x, y) is safe to move into at the given time step.

logic.location(x, y, time=None)

Proposition for the agent being at square (x, y), optionally at a given time step.

logic.implies(lhs, rhs)

Build the implication lhs ==> rhs as an Expr.

logic.equiv(lhs, rhs)

Build the biconditional lhs <=> rhs as an Expr.

logic.new_disjunction(sentences)

Combine a list of sentences into a single disjunction (their logical OR).

class logic.WumpusKB(dimrow)

Bases: PropKB

Create a Knowledge Base that contains the a temporal “Wumpus physics” and temporal rules with time zero.

make_action_sentence(action, time)

Tell the KB that action was taken at time and that no other action was.

make_percept_sentence(percept, time)

Tell the KB which of the five percepts hold (and which do not) at time.

add_temporal_sentences(time)

Add the successor-state axioms relating time to time - 1 (location, orientation, arrow possession and wumpus status). Does nothing for time == 0.

ask_if_true(query)

Return True if the KB entails query, decided via a SAT check on KB & ~query.

class logic.WumpusPosition(x, y, orientation)

Bases: object

A pose in the wumpus world: a square (x, y) together with an orientation.

get_location()

Return the (x, y) coordinates of this position.

set_location(x, y)

Set the (x, y) coordinates of this position.

get_orientation()

Return the orientation of this position.

set_orientation(orientation)

Set the orientation of this position.

class logic.HybridWumpusAgent(dimensions)

Bases: Agent

[Figure 7.20] An agent for the wumpus world that does logical inference.

execute(percept)

Update the KB with percept, infer the current state, and return the next action.

Implements the agent program: it deduces the current pose and safe squares, then either grabs the gold, explores unvisited safe squares, shoots at a possible wumpus, takes a calculated risk, or heads home and climbs out.

plan_route(current, goals, allowed)

Return an action sequence from current to any of goals through allowed squares, found by A* search.

plan_shot(current, goals, allowed)

Return an action sequence that moves to a square lined up with a possible wumpus and shoots.

logic.SAT_plan(init, transition, goal, t_max, SAT_solver=<function cdcl_satisfiable>)

[Figure 7.22] Converts a planning problem to Satisfaction problem by translating it to a cnf sentence. >>> transition = {‘A’: {‘Left’: ‘A’, ‘Right’: ‘B’}, ‘B’: {‘Left’: ‘A’, ‘Right’: ‘C’}, ‘C’: {‘Left’: ‘B’, ‘Right’: ‘C’}} >>> SAT_plan(‘A’, transition, ‘C’, 1) is None True

logic.unify(x, y, s={})

[Figure 9.1] 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. >>> unify(x, 3, {}) {x: 3}

logic.is_variable(x)

A variable is an Expr with no args and a lowercase symbol as the op.

logic.unify_var(var, x, s)

Unify the variable var with x under substitution s.

Follows existing bindings, applies the occur-check to avoid cyclic bindings, and returns the extended substitution (or None if unification fails).

logic.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).

logic.subst(s, x)

Substitute the substitution s into the expression x. >>> subst({x: 42, y:0}, F(x) + y) (F(42) + 0)

logic.cascade_substitution(s)

This method allows to return a correct unifier in normal form and perform a cascade substitution to s. For every mapping in s perform a cascade substitution on s.get(x) and if it is replaced with a function ensure that all the function terms are correct updates by passing over them again. >>> s = {x: y, y: G(z)} >>> cascade_substitution(s) >>> s == {x: G(z), y: G(z)} True

logic.unify_mm(x, y, s={})

Unify expressions x,y with substitution s using an efficient rule-based unification algorithm by Martelli & Montanari; 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. >>> unify_mm(x, 3, {}) {x: 3}

logic.term_reduction(x, y, s)

Apply term reduction to x and y if both are functions and the two root function symbols are equals (e.g. F(x1, x2, …, xn) and F(x1’, x2’, …, xn’)) by returning a new mapping obtained by replacing x: y with {x1: x1’, x2: x2’, …, xn: xn’}

logic.vars_elimination(x, s)

Apply variable elimination to x: if x is a variable and occurs in s, return the term mapped by x, else if x is a function recursively applies variable elimination to each term of the function.

logic.standardize_variables(sentence, dic=None)

Replace all the variables in sentence with new variables.

logic.parse_clauses_from_dimacs(dimacs_cnf)

Converts a string into CNF clauses according to the DIMACS format used in SAT competitions

class logic.FolKB(clauses=None)

Bases: 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

tell(sentence)

Add a definite clause to the KB, raising an exception if it is not one.

ask_generator(query)

Yield substitutions under which the KB entails query (via backward chaining).

retract(sentence)

Remove the given clause from the KB.

fetch_rules_for_goal(goal)

Return the clauses that could be used to prove goal (here, all clauses).

logic.fol_fc_ask(kb, alpha)

[Figure 9.3] A simple forward-chaining algorithm.

logic.fol_bc_ask(kb, query)

[Figure 9.6] A simple backward-chaining algorithm for first-order logic. KB should be an instance of FolKB, and query an atomic sentence.

logic.fol_bc_or(kb, goal, theta)

Backward-chaining OR step: yield substitutions proving goal via some rule in kb.

See [Figure 9.6].

logic.fol_bc_and(kb, goals, theta)

Backward-chaining AND step: yield substitutions proving every goal in goals.

See [Figure 9.6].

logic.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))

logic.simp(x)

Simplify the expression x.

logic.d(y, x)

Differentiate and then simplify. >>> d(x * x - x, x) ((2 * x) - 1)

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

class logic4e.KB(sentence=None)

Bases: object

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.

tell(sentence)

Add the sentence to the KB.

ask(query)

Return a substitution that makes the query true, or, failing that, return False.

ask_generator(query)

Yield all the substitutions that make query true.

retract(sentence)

Remove sentence from the KB.

class logic4e.PropKB(sentence=None)

Bases: KB

A KB for propositional logic. Inefficient, with no indexing.

tell(sentence)

Add the sentence’s clauses to the KB.

ask_generator(query)

Yield the empty substitution {} if KB entails query; else no results.

ask_if_true(query)

Return True if the KB entails query, else return False.

retract(sentence)

Remove the sentence’s clauses from the KB.

logic4e.KB_AgentProgram(KB)

A generic logical knowledge-based agent program. [Figure 7.1]

logic4e.facing_east(time)

Return the proposition that the agent is facing east at the given time.

logic4e.facing_west(time)

Return the proposition that the agent is facing west at the given time.

logic4e.facing_north(time)

Return the proposition that the agent is facing north at the given time.

logic4e.facing_south(time)

Return the proposition that the agent is facing south at the given time.

logic4e.wumpus(x, y)

Return the proposition that the Wumpus is in room (x, y).

logic4e.pit(x, y)

Return the proposition that there is a pit in room (x, y).

logic4e.breeze(x, y)

Return the proposition that there is a breeze in room (x, y).

logic4e.stench(x, y)

Return the proposition that there is a stench in room (x, y).

logic4e.wumpus_alive(time)

Return the proposition that the Wumpus is alive at the given time.

logic4e.have_arrow(time)

Return the proposition that the agent still has the arrow at the given time.

logic4e.percept_stench(time)

Return the proposition that the agent perceives a stench at the given time.

logic4e.percept_breeze(time)

Return the proposition that the agent perceives a breeze at the given time.

logic4e.percept_glitter(time)

Return the proposition that the agent perceives glitter at the given time.

logic4e.percept_bump(time)

Return the proposition that the agent perceives a bump at the given time.

logic4e.percept_scream(time)

Return the proposition that the agent perceives a scream at the given time.

logic4e.move_forward(time)

Return the proposition that the agent moves forward at the given time.

logic4e.shoot(time)

Return the proposition that the agent shoots the arrow at the given time.

logic4e.turn_left(time)

Return the proposition that the agent turns left at the given time.

logic4e.turn_right(time)

Return the proposition that the agent turns right at the given time.

logic4e.ok_to_move(x, y, time)

Return the proposition that room (x, y) is safe to move into at the given time.

logic4e.location(x, y, time=None)

Return the proposition that the agent is at room (x, y), optionally at a given time.

logic4e.implies(lhs, rhs)

Return the implication lhs ==> rhs as an Expr.

logic4e.equiv(lhs, rhs)

Return the biconditional lhs <=> rhs as an Expr.

logic4e.new_disjunction(sentences)

Return the disjunction (|) of all the sentences in the given list.

logic4e.is_symbol(s)

A string s is a symbol if it starts with an alphabetic char. >>> is_symbol(‘R2D2’) True

logic4e.is_var_symbol(s)

A logic variable symbol is an initial-lowercase string. >>> is_var_symbol(‘EXE’) False

logic4e.is_prop_symbol(s)

A proposition logic symbol is an initial-uppercase string. >>> is_prop_symbol(‘exe’) False

logic4e.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

logic4e.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

logic4e.parse_definite_clause(s)

Return the antecedents and the consequent of a definite clause.

logic4e.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

logic4e.tt_check_all(kb, alpha, symbols, model)

Auxiliary routine to implement tt_entails.

logic4e.prop_symbols(x)

Return the set of all propositional symbols in x.

logic4e.constant_symbols(x)

Return the set of all constant symbols in x.

logic4e.predicate_symbols(x)

Return a set of (symbol_name, arity) in x. All symbols (even functional) with arity > 0 are considered.

logic4e.tt_true(s)

Is a propositional sentence a tautology? >>> tt_true(‘P | ~P’) True

logic4e.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

logic4e.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)

logic4e.eliminate_implications(s)

Change implications into equivalent form with only &, |, and ~ as logical operators.

logic4e.move_not_inwards(s)

Rewrite sentence s by moving negation sign inward. >>> move_not_inwards(~(A | B)) (~A & ~B)

logic4e.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))

logic4e.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))

logic4e.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]

logic4e.conjuncts(s)

Return a list of the conjuncts in the sentence s. >>> conjuncts(A & B) [A, B] >>> conjuncts(A | B) [(A | B)]

logic4e.disjuncts(s)

Return a list of the disjuncts in the sentence s. >>> disjuncts(A | B) [A, B] >>> disjuncts(A & B) [(A & B)]

logic4e.pl_resolution(KB, alpha)

Propositional-logic resolution: say if alpha follows from KB. [Figure 7.12] >>> pl_resolution(horn_clauses_KB, A) True

logic4e.pl_resolve(ci, cj)

Return all clauses that can be obtained by resolving clauses ci and cj.

class logic4e.PropDefiniteKB(sentence=None)

Bases: PropKB

A KB of propositional definite clauses.

tell(sentence)

Add a definite clause to this KB.

ask_generator(query)

Yield the empty substitution if KB implies query; else nothing.

retract(sentence)

Remove the given definite clause from this KB.

clauses_with_premise(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.

logic4e.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

logic4e.wumpus_world_inference = ((B11 <=> (P12 | P21)) & ~B11)

[Figure 7.16] Propositional Logic Forward Chaining example

logic4e.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

logic4e.dpll(clauses, symbols, model)

See if the clauses are true in a partial model.

logic4e.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)

logic4e.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)

logic4e.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)

logic4e.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)

logic4e.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

class logic4e.WumpusKB(dimrow)

Bases: PropKB

Create a Knowledge Base that contains the atemporal “Wumpus physics” and temporal rules with time zero.

make_action_sentence(action, time)

Tell the KB which action is taken at the given time (asserting that one and negating all the others).

make_percept_sentence(percept, time)

Tell the KB the percept observed at the given time, asserting each perceived fluent (Glitter, Bump, Stench, Breeze, Scream) and negating the unperceived ones.

add_temporal_sentences(time)

Tell the KB the successor-state axioms relating the world at the given time to the previous time step (location, orientation, last action, arrow and Wumpus state).

ask_if_true(query)

Return True if the KB entails the query, using propositional resolution.

class logic4e.WumpusPosition(x, y, orientation)

Bases: object

A position in the wumpus world: a room (x, y) plus a facing orientation.

get_location()

Return the (x, y) coordinates of this position.

set_location(x, y)

Set the (x, y) coordinates of this position.

get_orientation()

Return the facing orientation of this position.

set_orientation(orientation)

Set the facing orientation of this position.

class logic4e.HybridWumpusAgent(dimensions)

Bases: Agent

An agent for the wumpus world that does logical inference. [Figure 7.20]

execute(percept)

Update the KB with the current percept, infer the agent’s state, and return the next action, building or following a plan to grab the gold, explore safe unvisited rooms, shoot the Wumpus, or climb out.

plan_route(current, goals, allowed)

Return a sequence of actions that moves from the current position to one of the goals, staying within the allowed (safe) rooms, found with A* search.

plan_shot(current, goals, allowed)

Return a sequence of actions that moves to a room lined up with a possible Wumpus location and then shoots, staying within the allowed (safe) rooms.

logic4e.SAT_plan(init, transition, goal, t_max, SAT_solver=<function 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

logic4e.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}

logic4e.is_variable(x)

A variable is an Expr with no args and a lowercase symbol as the op.

logic4e.unify_var(var, x, s)

Unify the variable var with x under substitution s, returning the extended substitution, or None if the occur-check fails.

logic4e.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).

logic4e.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

class logic4e.FolKB(initial_clauses=None)

Bases: 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

tell(sentence)

Add a first-order definite clause to the KB, raising if it is not definite.

ask_generator(query)

Yield each substitution that makes the query true, via backward chaining.

retract(sentence)

Remove the given clause from the KB.

fetch_rules_for_goal(goal)

Return the clauses that could be used to prove the goal (here, all clauses).

logic4e.fol_fc_ask(KB, alpha)

A simple forward-chaining algorithm. [Figure 9.3]

logic4e.subst(s, x)

Substitute the substitution s into the expression x. >>> subst({x: 42, y:0}, F(x) + y) (F(42) + 0)

logic4e.standardize_variables(sentence, dic=None)

Replace all the variables in sentence with new variables.

logic4e.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.

logic4e.fol_bc_or(KB, goal, theta)

Yield each substitution extending theta that proves the goal by unifying it with the head of some standardized rule and recursively proving that rule’s premises.

logic4e.fol_bc_and(KB, goals, theta)

Yield each substitution extending theta that proves all the given goals in conjunction by backward chaining.

logic4e.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))

logic4e.simp(x)

Simplify the expression x.

logic4e.d(y, x)

Differentiate and then simplify. >>> d(x * x - x, x) ((2 * x) - 1)

Knowledge in learning (Chapter 19)

knowledge.current_best_learning(examples, h, examples_so_far=None)

[Figure 19.2] The hypothesis is a list of dictionaries, with each dictionary representing a disjunction.

knowledge.specializations(examples_so_far, h)

Specialize the hypothesis by adding AND operations to the disjunctions

knowledge.generalizations(examples_so_far, h)

Generalize the hypothesis. First delete operations (including disjunctions) from the hypothesis. Then, add OR operations.

knowledge.add_or(examples_so_far, h)

Add an OR operation to the hypothesis. The AND operations in the disjunction are generated by the last example (which is the problematic one).

knowledge.version_space_learning(examples)

[Figure 19.3] The version space is a list of hypotheses, which in turn are a list of dictionaries/disjunctions.

knowledge.version_space_update(V, e)

Return the version space V restricted to the hypotheses that remain consistent with example e.

knowledge.all_hypotheses(examples)

Build a list of all the possible hypotheses

knowledge.values_table(examples)

Build a table with all the possible values for each attribute. Returns a dictionary with keys the attribute names and values a list with the possible values for the corresponding attribute.

knowledge.build_attr_combinations(s, values)

Given a set of attributes, builds all the combinations of values. If the set holds more than one attribute, recursively builds the combinations.

knowledge.build_h_combinations(hypotheses)

Given a set of hypotheses, builds and returns all the combinations of the hypotheses.

knowledge.minimal_consistent_det(E, A)

Return a minimal set of attributes which give consistent determination

knowledge.consistent_det(A, E)

Check if the attributes(A) is consistent with the examples(E)

class knowledge.FOILContainer(clauses=None)

Bases: FolKB

Hold the kb and other necessary elements required by FOIL.

tell(sentence)

Add a definite clause to the knowledge base, recording its constant and predicate symbols; raise an exception if it is not a definite clause.

foil(examples, target)

Learn a list of first-order horn clauses ‘examples’ is a tuple: (positive_examples, negative_examples). positive_examples and negative_examples are both lists which contain substitutions.

new_clause(examples, target)

Find a horn clause which satisfies part of the positive examples but none of the negative examples. The horn clause is specified as [consequent, list of antecedents] Return value is the tuple (horn_clause, extended_positive_examples).

extend_example(example, literal)

Generate extended examples which satisfy the literal.

new_literals(clause)

Generate new literals based on known predicate symbols. Generated literal must share at least one variable with clause

choose_literal(literals, examples)

Choose the best literal based on the information gain.

gain(l, examples)

Find the utility of each literal when added to the body of the clause. Utility function is:

gain(R, l) = T * (log_2 (post_pos / (post_pos + post_neg)) - log_2 (pre_pos / (pre_pos + pre_neg)))

where:

pre_pos = number of positive bindings of rule R (=current set of rules)
pre_neg = number of negative bindings of rule R
post_pos = number of positive bindings of rule R' (= R U {l} )
post_neg = number of negative bindings of rule R'
T = number of positive bindings of rule R that are still covered
    after adding literal l

update_examples(target, examples, extended_examples)

Add to the kb those examples what are represented in extended_examples List of omitted examples is returned.

knowledge.check_all_consistency(examples, h)

Check for the consistency of all examples under h.

knowledge.check_negative_consistency(examples, h)

Check if the negative examples are consistent under h.

knowledge.disjunction_value(e, d)

The value of example e under disjunction d.

knowledge.guess_value(e, h)

Guess value of example e under hypothesis h.

knowledge.is_consistent(e, h)

Return True iff hypothesis h predicts the same value as example e’s actual GOAL label.

knowledge.false_positive(e, h)

Return True iff h predicts True for e while its actual GOAL is False.

knowledge.false_negative(e, h)

Return True iff h predicts False for e while its actual GOAL is True.