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, imported from utils, 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 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 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.

KBAgentProgram(kb)

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

is_symbol(s)

A string s is a symbol if it starts with an alphabetic char.

is_var_symbol(s)

A logic variable symbol is an initial-lowercase string.

is_prop_symbol(s)

A proposition logic symbol is an initial-uppercase string.

gensym(prefix='s_')

Return a fresh logic symbol with a unique name, like Lisp’s gensym [#230].

Successive calls return distinct symbols s_0, s_1, s_2, … – handy for building an array or dict of symbols, or for standardizing apart. Pass a prefix to control the name stem.

variables(s)

Return a set of the variables in expression s.

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.

parse_definite_clause(s)

Return the antecedents and the consequent of a definite clause.

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_check_all(kb, alpha, symbols, model)

Auxiliary routine to implement tt_entails.

prop_symbols(x)

Return the set of all propositional symbols in x.

constant_symbols(x)

Return the set of all constant symbols in x.

predicate_symbols(x)

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

tt_true(s)

Is a propositional sentence a tautology?

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.

to_cnf(s)

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

eliminate_implications(s)

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

move_not_inwards(s)

Rewrite sentence s by moving negation sign inward.

distribute_and_over_or(s)

Given a sentence s consisting of conjunctions and disjunctions of literals, return an equivalent sentence in CNF.

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.

dissociate(op, args)

Given an associative op, return a flattened list result such that Expr(op, *result) means the same as Expr(op, *args).

conjuncts(s)

Return a list of the conjuncts in the sentence s.

disjuncts(s)

Return a list of the disjuncts in the sentence s.

pl_resolution(kb, alpha)

[Figure 7.12] Propositional-logic resolution: say if alpha follows from KB.

pl_resolve(ci, cj)

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

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

pl_fc_entails(kb, q)

[Figure 7.15] Use forward chaining to see if a PropDefiniteKB entails symbol q.

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

[Figure 7.16] Propositional Logic Forward Chaining example

no_branching_heuristic(symbols, clauses)

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

min_clauses(clauses)

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

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

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

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

zm(symbols, clauses)

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

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)

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

jw(symbols, clauses)

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

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

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(clauses, symbols, model, branching_heuristic=<function no_branching_heuristic>)

[Figure 7.17] The Davis-Putnam-Logemann-Loveland procedure: decide whether clauses are satisfiable by depth-first assignment of symbols, accelerated by the pure-symbol and unit-clause heuristics (plus an optional branching heuristic). Returns the satisfying model, or False.

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_unit_clause(clauses, model)

Find a forced assignment if possible from a clause with only 1 variable not bound in the model.

unit_clause_assign(clause, model)

Return a single variable/value pair that makes clause true in the model, if possible.

inspect_literal(literal)

The symbol in this literal, and the value it should take to make the literal true.

no_restart(conflicts, restarts, queue_lbd, sum_lbd)

Default CDCL restart policy: never restart.

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

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

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

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

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.

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.

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.

pl_binary_resolution(ci, cj)

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

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

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

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

WalkSAT(clauses, p=0.5, max_flips=10000)

Checks for satisfiability of all clauses by randomly flipping values of variables

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.

facing_east(time)

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

facing_west(time)

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

facing_north(time)

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

facing_south(time)

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

wumpus(x, y)

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

pit(x, y)

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

breeze(x, y)

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

stench(x, y)

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

wumpus_alive(time)

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

have_arrow(time)

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

percept_stench(time)

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

percept_breeze(time)

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

percept_glitter(time)

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

percept_bump(time)

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

percept_scream(time)

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

move_forward(time)

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

shoot(time)

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

turn_left(time)

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

turn_right(time)

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

ok_to_move(x, y, time)

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

location(x, y, time=None)

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

implies(lhs, rhs)

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

equiv(lhs, rhs)

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

new_disjunction(sentences)

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

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

A single square can yield several percepts at once (e.g. a Stench and a Breeze), so percept may be one percept object or a collection of them (the format produced by WumpusEnvironment.percept); None means nothing was perceived.

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

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.

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.

is_variable(x)

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

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

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

subst(s, x)

Substitute the substitution s into the expression x.

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.

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.

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’}

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.

standardize_variables(sentence, dic=None)

Replace all the variables in sentence with new variables.

parse_clauses_from_dimacs(dimacs_cnf)

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

class FolKB(clauses=None)

Bases: KB

A knowledge base consisting of first-order definite clauses.

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

fol_fc_ask(kb, alpha)

[Figure 9.3] A simple forward-chaining algorithm.

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.

fol_bc_or(kb, goal, theta)

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

See [Figure 9.6].

fol_bc_and(kb, goals, theta)

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

See [Figure 9.6].

diff(y, x)

Return the symbolic derivative, dy/dx, as an Expr. However, you probably want to simplify the results with simp.

simp(x)

Simplify the expression x.

d(y, x)

Differentiate and then simplify.

Knowledge in learning (Chapter 19)

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.

specializations(examples_so_far, h)

Specialize the hypothesis by adding AND operations to the disjunctions

generalizations(examples_so_far, h)

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

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

version_space_learning(examples)

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

version_space_update(V, e)

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

all_hypotheses(examples)

Build a list of all the possible hypotheses

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.

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.

build_h_combinations(hypotheses)

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

minimal_consistent_det(E, A)

Return a minimal set of attributes which give consistent determination

consistent_det(A, E)

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

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

check_all_consistency(examples, h)

Check for the consistency of all examples under h.

check_negative_consistency(examples, h)

Check if the negative examples are consistent under h.

disjunction_value(e, d)

The value of example e under disjunction d.

guess_value(e, h)

Guess value of example e under hypothesis h.

is_consistent(e, h)

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

false_positive(e, h)

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

false_negative(e, h)

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