This is a replacement for sympy.core.logic and will be used
extensively by the query module. The old logic module can be
removed once the old assumption system is removed.
Contents
--------
sympy.logic.boolalg
- Operators for boolean algebra on symbols {And: &, Or: |, Not: ~}
- some useful methods, mainly used to convert expressions to
conjunctive normal form (CNF)
sympy.logic.inference
- Rules for inference in propositional logic. Main method here is
satisfiable(expr), which checks satisfiability of a propositional
sentence (for now using dpll algorithm)
sympy.logic.kb
- Definition of a knowledge base
sympy.algorithms
- some algorithms used by higher order methods (just DPLL for now),
but in a future we should also have Quine-McCluskey for simplification
of boolean expressions
Most of the methods in this module are implementations of algorithms described
in the book "AI: A modern approach", http://aima.cs.berkeley.edu/
---
sympy/core/basic.py | 26 ++++++-
sympy/logic/__init__.py | 2 +
sympy/logic/algorithms/dpll.py | 49 +++++++++++
sympy/logic/boolalg.py | 155 +++++++++++++++++++++++++++++++++++
sympy/logic/inference.py | 119 +++++++++++++++++++++++++++
sympy/logic/kb.py | 36 ++++++++
sympy/logic/tests/test_boolalg.py | 110 +++++++++++++++++++++++++
sympy/logic/tests/test_inference.py | 46 ++++++++++
8 files changed, 541 insertions(+), 2 deletions(-)
create mode 100644 sympy/logic/__init__.py
create mode 100644 sympy/logic/algorithms/__init__.py
create mode 100644 sympy/logic/algorithms/dpll.py
create mode 100755 sympy/logic/boolalg.py
create mode 100755 sympy/logic/inference.py
create mode 100644 sympy/logic/kb.py
create mode 100755 sympy/logic/tests/test_boolalg.py
create mode 100755 sympy/logic/tests/test_inference.py
diff --git a/sympy/core/basic.py b/sympy/core/basic.py
index b48e633..6ab3101 100644
--- a/sympy/core/basic.py
+++ b/sympy/core/basic.py
@@ -680,8 +680,30 @@ def __rdiv__(self, other):
__truediv__ = __div__
__rtruediv__ = __rdiv__
-
-
+ # *******************
+ # * Logic operators *
+ # *******************
+
+ def __and__(self, other):
+ """Overloading for & operator"""
+ from sympy.logic.boolalg import And
+ return And(self, other)
+ def __or__(self, other):
+ """Overloading for |"""
+ from sympy.logic.boolalg import Or
+ return Or(self, other)
+ def __invert__(self):
+ """Overloading for ~"""
+ from sympy.logic.boolalg import Not
+ return Not(self)
+ def __rshift__(self, other):
+ """Overloading for >>"""
+ from sympy.logic.boolalg import Implies
+ return Implies(self, other)
+ def __lshift__(self, other):
+ """Overloading for <<"""
+ from sympy.logic.boolalg import Implies
+ return Implies(other, self)
def __repr__(self):
diff --git a/sympy/logic/__init__.py b/sympy/logic/__init__.py
new file mode 100644
index 0000000..5076249
--- /dev/null
+++ b/sympy/logic/__init__.py
@@ -0,0 +1,2 @@
+from boolalg import *
+from inference import *
\ No newline at end of file
diff --git a/sympy/logic/algorithms/__init__.py
b/sympy/logic/algorithms/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/sympy/logic/algorithms/dpll.py b/sympy/logic/algorithms/dpll.py
new file mode 100644
index 0000000..77d92ed
--- /dev/null
+++ b/sympy/logic/algorithms/dpll.py
@@ -0,0 +1,49 @@
+from sympy.core import Symbol
+from sympy.logic.boolalg import conjuncts, to_cnf
+from sympy.logic.inference import find_pure_symbol, find_unit_clause, pl_true
+
+def dpll_satisfiable(expr):
+ """Check satisfiability of a propositional sentence.
+ It returns a model rather than True when it succeeds
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> dpll_satisfiable(A & ~B)
+ {A: True, B: False}
+ >>> dpll_satisfiable(A & ~A)
+ False
+
+ References: Implemented as described in http://aima.cs.berkeley.edu/
+ """
+ clauses = conjuncts(to_cnf(expr))
+ symbols = list(expr.atoms(Symbol))
+ return dpll(clauses, symbols, {})
+
+def dpll(clauses, symbols, model):
+ """See if the clauses are true in a partial model.
+ http://en.wikipedia.org/wiki/DPLL_algorithm
+ """
+ unknown_clauses = [] ## clauses with an unknown truth value
+ for c in clauses:
+ val = pl_true(c, model)
+ if val == False:
+ return False
+ if val != True:
+ unknown_clauses.append(c)
+ if not unknown_clauses:
+ return model
+ P, value = find_pure_symbol(symbols, unknown_clauses)
+ if P:
+ model.update({P: value})
+ syms = [x for x in symbols if x != P]
+ return dpll(clauses, syms, model)
+ P, value = find_unit_clause(clauses, model)
+ if P:
+ model.update({P: value})
+ syms = [x for x in symbols if x != P]
+ return dpll(clauses, syms, model)
+ P = symbols.pop()
+ model_1, model_2 = model.copy(), model.copy()
+ model_1.update({P: True})
+ model_2.update({P: False})
+ return (dpll(clauses, symbols, model_1) or
+ dpll(clauses, symbols, model_2))
\ No newline at end of file
diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py
new file mode 100755
index 0000000..1a57740
--- /dev/null
+++ b/sympy/logic/boolalg.py
@@ -0,0 +1,155 @@
+"""Boolean algebra module for SymPy"""
+from sympy.core import Basic, Function, sympify, Symbol
+from sympy.utilities import flatten
+
+
+class BooleanFunction(Function):
+ """Boolean function is a function that lives in a boolean space
+ It is used as base class for And, Or, Not, etc.
+ """
+ pass
+
+class And(BooleanFunction):
+ """Evaluates to True if all it's arguments are True,
+ False otherwise"""
+ @classmethod
+ def eval(cls, *args):
+ if len(args) < 2: raise ValueError("And must have at least two
arguments")
+ out_args = []
+ for i, arg in enumerate(args): # we iterate over a copy or args
+ if isinstance(arg, bool):
+ if not arg: return False
+ else: continue
+ out_args.append(arg)
+ if len(out_args) == 0: return True
+ if len(out_args) == 1: return out_args[0]
+ sargs = sorted(flatten(out_args, cls=cls))
+ return Basic.__new__(cls, *sargs)
+
+class Or(BooleanFunction):
+ @classmethod
+ def eval(cls, *args):
+ if len(args) < 2: raise ValueError("And must have at least two
arguments")
+ out_args = []
+ for i, arg in enumerate(args): # we iterate over a copy or args
+ if isinstance(arg, bool):
+ if arg: return True
+ else: continue
+ out_args.append(arg)
+ if len(out_args) == 0: return False
+ if len(out_args) == 1: return out_args[0]
+ sargs = sorted(flatten(out_args, cls=cls))
+ return Basic.__new__(cls, *sargs)
+
+class Not(BooleanFunction):
+ """De Morgan rules applied automatically, so Not is moved inward"""
+ @classmethod
+ def eval(cls, *args):
+ if len(args) > 1:
+ return map(cls, args)
+ arg = args[0]
+ # apply De Morgan Rules
+ if isinstance(arg, And):
+ return Or( *[Not(a) for a in arg.args])
+ if isinstance(arg, Or):
+ return And(*[Not(a) for a in arg.args])
+ if isinstance(arg, bool): return not arg
+ if isinstance(arg, Not):
+ if len(arg.args) == 1: return arg.args[0]
+ return arg.args
+
+class Implies(BooleanFunction):
+ def __init__(self, *args, **kwargs):
+ if len(args) != 2: raise ValueError("Wrong set of arguments")
+ return super(BooleanFunction, self).__init__(*args, **kwargs)
+
+class Equivalent(BooleanFunction):
+ pass
+
+### end class definitions. Some useful methods
+
+def conjuncts(expr):
+ """Return a list of the conjuncts in the expr s.
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> conjuncts(A & B)
+ [A, B]
+ >>> conjuncts(A | B)
+ [Or(A, B)]
+ """
+ if isinstance(expr, And):
+ return list(expr.args)
+ else:
+ return [expr]
+
+def disjuncts(expr):
+ """Return a list of the disjuncts in the sentence s.
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> disjuncts(A | B)
+ [A, B]
+ >>> disjuncts(A & B)
+ [And(A, B)]
+ """
+ if isinstance(expr, Or):
+ return list(expr.args)
+ else:
+ return [expr]
+
+def distribute_and_over_or(expr):
+ """Given a sentence s consisting of conjunctions and disjunctions
+ of literals, return an equivalent sentence in CNF.
+ """
+ if isinstance(expr, Or):
+ expr = Or(*expr.args)
+ if len(expr.args) == 0:
+ return False
+ if len(expr.args) == 1:
+ return distribute_and_over_or(expr.args[0])
+ for arg in expr.args:
+ if isinstance(arg, And):
+ conj = arg
+ break
+ else: return type(expr)(*expr.args)
+ others = [a for a in expr.args if a is not conj]
+ if len(others) == 1:
+ rest = others[0]
+ else:
+ rest = Or(*others)
+ return And(*map(distribute_and_over_or,
+ [Or(c, rest) for c in conj.args]))
+ elif isinstance(expr, And):
+ return And(*map(distribute_and_over_or, expr.args))
+ else:
+ return expr
+
+def to_cnf(expr):
+ """Convert a propositional logical sentence s to conjunctive normal form.
+ That is, of the form ((A | ~B | ...) & (B | C | ...) & ...)
+ """
+ expr = sympify(expr)
+ expr = eliminate_implications(expr)
+ return distribute_and_over_or(expr)
+
+def eliminate_implications(expr):
+ """Change >>, <<, and <=> into &, |, and ~. That is, return an Expr
+ that is equivalent to s, but has only &, |, and ~ as logical operators.
+ """
+ expr = sympify(expr)
+ if expr.is_Atom: return expr ## (Atoms are unchanged.)
+ args = map(eliminate_implications, expr.args)
+ a, b = args[0], args[-1] # TODO: multiple implications?
+ if isinstance(expr, Implies):
+ return Or(b, Not(a))
+ elif isinstance(expr, Equivalent):
+ return And(Or(a, Not(b)), Or(b, Not(a)))
+ else:
+ return type(expr)(*args)
+
+def compile_rule(s):
+ """Transforms a rule into a sympy expression
+ A rule is a string of the form "symbol1 & symbol2 | ..."
+ See sympy.assumptions.known_facts for examples of rules
+ """
+ import re
+ return eval(re.sub(r'([a-zA-Z0-9_.]+)', r'Symbol("\1")', s), {'Symbol' :
Symbol})
\ No newline at end of file
diff --git a/sympy/logic/inference.py b/sympy/logic/inference.py
new file mode 100755
index 0000000..a638ee2
--- /dev/null
+++ b/sympy/logic/inference.py
@@ -0,0 +1,119 @@
+"""Inference in propositional logic"""
+from sympy.core import Symbol
+from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent, disjuncts, \
+ to_cnf
+
+
+def find_pure_symbol(symbols, unknown_clauses):
+ """Find a symbol and its value if it appears only as a positive literal
+ (or only as a negative) in clauses.
+ >>> from sympy import symbols
+ >>> A, B, C = symbols('ABC')
+ >>> find_pure_symbol([A, B, C], [A|~B,~B|~C,C|A])
+ (A, True)
+ """
+ for sym in symbols:
+ found_pos, found_neg = False, False
+ for c in unknown_clauses:
+ if not found_pos and sym in disjuncts(c): found_pos = True
+ if not found_neg and Not(sym) in disjuncts(c): found_neg = True
+ if found_pos != found_neg: return sym, found_pos
+ return None, None
+
+def find_unit_clause(clauses, model):
+ """A unit clause has only 1 variable that is not bound in the model.
+ >>> from sympy import symbols
+ >>> A, B, C = symbols('ABC')
+ >>> find_unit_clause([A | B | C, B | ~C, A | ~B], {A:True})
+ (B, True)
+ """
+ for clause in clauses:
+ num_not_in_model = 0
+ for literal in disjuncts(clause):
+ sym = literal_symbol(literal)
+ if sym not in model:
+ num_not_in_model += 1
+ P, value = sym, (isinstance(literal, Not))
+ if num_not_in_model == 1:
+ return P, value
+ return None, None
+
+def literal_symbol(literal):
+ """The symbol in this literal (without the negation).
+ >>> from sympy import Symbol
+ >>> A = Symbol('A')
+ >>> literal_symbol(A)
+ A
+ >>> literal_symbol(~A)
+ A
+ """
+ if isinstance(literal, Not):
+ return literal.args[0]
+ else:
+ return literal
+
+def satisfiable(expr, algorithm="dpll"):
+ """Check satisfiability of a propositional sentence.
+ Returns a model when it succeeds
+
+ Examples
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> satisfiable(A & ~B)
+ {A: True, B: False}
+ >>> satisfiable(A & ~A)
+ False
+ """
+ expr = to_cnf(expr)
+ if algorithm == "dpll":
+ from sympy.logic.algorithms.dpll import dpll_satisfiable
+ return dpll_satisfiable(expr)
+ raise NotImplementedError
+
+def pl_true(expr, 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.
+
+ The model is implemented as a dict containing the pair symbol, boolean
value.
+
+ Examples:
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> pl_true( A & B, {A: True, B : True})
+ True
+ """
+ args = expr.args
+ if isinstance(expr, bool):
+ return expr
+ if expr.is_Atom: return model.get(expr)
+ elif isinstance(expr, Not):
+ p = pl_true(args[0], model)
+ if p is None: return None
+ else: return not p
+ elif isinstance(expr, Or):
+ result = False
+ for arg in args:
+ p = pl_true(arg, model)
+ if p == True: return True
+ if p == None: result = None
+ return result
+ elif isinstance(expr, And):
+ result = True
+ for arg in args:
+ p = pl_true(arg, model)
+ if p == False: return False
+ if p == None: result = None
+ return result
+ p, q = args
+ if isinstance(expr, Implies):
+ return pl_true(Or(Not(p), q), model)
+ pt = pl_true(p, model)
+ if pt == None: return None
+ qt = pl_true(q, model)
+ if qt == None: return None
+ if isinstance(expr, Equivalent):
+ return pt == qt
+ else:
+ raise ValueError, "Illegal operator in logic expression" + str(exp)
\ No newline at end of file
diff --git a/sympy/logic/kb.py b/sympy/logic/kb.py
new file mode 100644
index 0000000..267af91
--- /dev/null
+++ b/sympy/logic/kb.py
@@ -0,0 +1,36 @@
+from sympy.logic.boolalg import And, conjuncts, to_cnf
+from sympy.logic.inference import satisfiable
+
+class KB(object):
+ pass
+
+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(self, query):
+ """TODO: examples"""
+ if len(self.clauses) == 0: return {}
+ query_conjuncts = conjuncts(to_cnf(~query))
+ query_conjuncts.extend(self.clauses)
+ return not satisfiable(And(*query_conjuncts))
+
+ def ask_generator(self, query):
+ "Yield the empty substitution if KB implies query; else False"
+ if not tt_entails(Expr('&', *self.clauses), query):
+ return
+ yield {}
+
+ 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)
\ No newline at end of file
diff --git a/sympy/logic/tests/test_boolalg.py
b/sympy/logic/tests/test_boolalg.py
new file mode 100755
index 0000000..e4f1c32
--- /dev/null
+++ b/sympy/logic/tests/test_boolalg.py
@@ -0,0 +1,110 @@
+from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent, to_cnf, \
+ eliminate_implications, distribute_and_over_or
+from sympy import symbols
+from sympy.utilities.pytest import raises
+
+def test_overloading():
+ """Test that |, & are overloaded as expected"""
+ A, B, C = symbols('ABC')
+ assert A & B == And(A, B)
+ assert A | B == Or(A, B)
+ assert (A & B) | C == Or(And(A, B), C)
+ assert A >> B == Implies(A, B)
+ assert A << B == Implies(B, A)
+ assert ~A == Not(A)
+
+def test_bool_unary():
+ """Test boolean functions with one argument
+ Only Not is well defined in this case.
+ All other functions should raise a ValueError
+ """
+ A = symbols('A')
+ assert Not(True ) == False
+ assert Not(False) == True
+ raises(ValueError, "And(True)")
+ raises(ValueError, "And(False)")
+ raises(ValueError, "And(A)")
+ raises(ValueError, "Or(True)")
+ raises(ValueError, "Or(False)")
+ raises(ValueError, "Or(A)")
+
+def test_And_bool_2():
+ """Test And with two boolean arguments"""
+ assert And(True, True ) == True
+ assert And(True, False) == False
+ assert And(False, False) == False
+
+def test_Or_bool():
+ assert Or(True, True ) == True
+ assert Or(True, False) == True
+ assert Or(False, False) == False
+
+def test_Not_bool():
+ assert Not(True, True ) == [False, False]
+ assert Not(True, False) == [False, True ]
+ assert Not(False,False) == [True, True ]
+
+def test_Implies():
+ A, B, C = symbols('ABC')
+ raises(ValueError, "Implies()")
+ raises(ValueError, "Implies(A)")
+ raises(ValueError, "Implies(A, B, C)")
+
+def test_bool_symbol():
+ """Test that mixing symbols with boolean values
+ works as expected"""
+ A, B, C = symbols('ABC')
+ assert And(A, True) == A
+ assert And(A, True, True) == A
+ assert And(A, False) == False
+ assert And(A, True, False) == False
+ assert Or(A, True) == True
+ assert Or(A, False) == A
+
+"""
+we test for axioms of boolean algebra
+see http://en.wikipedia.org/wiki/Boolean_algebra_(structure)
+"""
+
+def test_commutative():
+ """Test for commutativity of And and Not"""
+ A, B = symbols('AB')
+ assert A & B == B & A
+ assert A | B == B | A
+
+def test_and_associativity():
+ """Test for associativity of And"""
+ A, B, C = symbols('ABC')
+ assert (A & B) & C == A & (B & C)
+
+def test_or_assicativity():
+ A, B, C = symbols('ABC')
+ assert ((A | B) | C) == (A | (B | C))
+
+def test_double_negation():
+ a = symbols('a')
+ assert ~(~a) == a
+
+def test_De_Morgan():
+ A, B = symbols('AB')
+ assert ~(A & B) == (~A) | (~B)
+ assert ~(A | B) == (~A) & (~B)
+
+
+# test methods
+def test_eliminate_implications():
+ A, B, C = symbols('ABC')
+ assert eliminate_implications( A >> B) == (~A) | B
+ assert eliminate_implications(A >> (C >>Not(B))) \
+ == Or(Or(Not(B), Not(C)), Not(A))
+
+def test_distribute():
+ A, B, C = symbols('ABC')
+ assert distribute_and_over_or(Or(And(A, B), C)) == And(Or(A, C), Or(B, C))
+
+
+def test_to_cnf():
+ A, B, C = symbols('ABC')
+ assert to_cnf(Not(Or(B, C))) == And(Not(B), Not(C))
+ assert to_cnf(Equivalent(A, Or(B,C))) == \
+ And(Or(Not(B), A), Or(Not(C), A), Or(B, C, Not(A)))
diff --git a/sympy/logic/tests/test_inference.py
b/sympy/logic/tests/test_inference.py
new file mode 100755
index 0000000..6667e15
--- /dev/null
+++ b/sympy/logic/tests/test_inference.py
@@ -0,0 +1,46 @@
+from sympy import symbols
+from sympy.logic.boolalg import And, Not, Or, Equivalent, Implies, to_cnf
+from sympy.logic.inference import pl_true, satisfiable
+from sympy.logic.algorithms.dpll import dpll
+from sympy.logic.kb import PropKB
+
+
+def test_satisfiable():
+ A, B, C = symbols('ABC')
+ assert satisfiable( A & ~A ) == False
+ assert satisfiable( A & ~B ) == {A: True, B: False}
+ assert satisfiable( A & B & C ) == {A: True, B: True, C: True}
+ assert satisfiable( A | B ) in ({A: True}, {B: True})
+
+def test_satisfiable_1():
+ """We prove expr entails alpha proving expr & ~B is unsatisfiable"""
+ A, B, C = symbols('ABC')
+ assert satisfiable(A & (A >> B) & ~B) == False
+
+def test_pl_true():
+ A, B, C = symbols('ABC')
+ assert pl_true( And(A, B), {A : True, B : True}) == True
+ assert pl_true( Or(A, B), {A : True}) == True
+ assert pl_true( Or(A, B), {B : True}) == True
+
+ # test for false
+ assert pl_true ( And(A, B), {A: False, B: False}) == False
+ assert pl_true ( And(A, B), {A: False}) == False
+ assert pl_true ( And(A, B), {B: False}) == False
+ assert pl_true ( Or(A, B), {A: False, B: False}) == False
+
+def test_PropKB():
+ A, B, C = symbols('ABC')
+ kb = PropKB()
+ kb.tell(A)
+ kb.tell(A >> B)
+ kb.tell(B >> C)
+ assert kb.ask(B) == True
+ assert kb.ask(C) == True
+ "TODO: test for api: .clauses etc"
+
+def test_propKB_tolerant():
+ """"Test that it is tolerant to bad input"""
+ kb = PropKB()
+ A, B, C = symbols('ABC')
+ assert kb.ask(B) == {}
--
1.6.1.2
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups
"sympy-patches" group.
To post to this group, send email to sympy-patches@googlegroups.com
To unsubscribe from this group, send email to
sympy-patches+unsubscr...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/sympy-patches?hl=en
-~----------~----~----~----~------~----~------~--~---
