/usr/share/pyshared/sympy/logic/inference.py is in python-sympy 0.7.1.rc1-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 | """Inference in propositional logic"""
from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent, \
conjuncts, to_cnf
from sympy.core.basic import C
from sympy.core.sympify import sympify
def literal_symbol(literal):
"""The symbol in this literal (without the negation).
>>> from sympy import Symbol
>>> from sympy.abc import A
>>> from sympy.logic.inference import literal_symbol
>>> literal_symbol(A)
A
>>> literal_symbol(~A)
A
"""
if literal.func is Not:
return literal.args[0]
else:
return literal
def satisfiable(expr, algorithm="dpll2"):
"""Check satisfiability of a propositional sentence.
Returns a model when it succeeds
Examples
>>> from sympy.abc import A, B
>>> from sympy.logic.inference import satisfiable
>>> 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)
elif algorithm == "dpll2":
from sympy.logic.algorithms.dpll2 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.abc import A, B
>>> from sympy.logic.inference import pl_true
>>> pl_true( A & B, {A: True, B : True})
True
"""
if isinstance(expr, bool):
return expr
expr = sympify(expr)
if expr.is_Atom:
return model.get(expr)
args = expr.args
if expr.func is Not:
p = pl_true(args[0], model)
if p is None: return None
else: return not p
elif expr.func is 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 expr.func is And:
result = True
for arg in args:
p = pl_true(arg, model)
if p == False: return False
if p == None: result = None
return result
elif expr.func is Implies:
p, q = args
return pl_true(Or(Not(p), q), model)
elif expr.func is Equivalent:
p, q = args
pt = pl_true(p, model)
if pt == None:
return None
qt = pl_true(q, model)
if qt == None:
return None
return pt == qt
else:
raise ValueError("Illegal operator in logic expression" + str(expr))
class KB(object):
"""Base class for all knowledge bases"""
def __init__(self, sentence=None):
self.clauses = []
if sentence:
self.tell(sentence)
def tell(self, sentence):
raise NotImplementedError
def ask(self, query):
raise NotImplementedError
def retract(self, sentence):
raise NotImplementedError
class PropKB(KB):
"A KB for Propositional Logic. Inefficient, with no indexing."
def tell(self, sentence):
"Add the sentence's clauses to the KB"
for c in conjuncts(to_cnf(sentence)):
if not c in self.clauses: self.clauses.append(c)
def ask(self, query):
"""TODO: examples"""
if len(self.clauses) == 0: return False
from sympy.logic.algorithms.dpll import dpll
query_conjuncts = self.clauses[:]
query_conjuncts.extend(conjuncts(to_cnf(query)))
s = set()
for q in query_conjuncts:
s = s.union(q.atoms(C.Symbol))
return bool(dpll(query_conjuncts, list(s), {}))
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)
|