"""Inference in propositional logic"""
from __future__ import print_function, division
from sympy.logic.boolalg import And, Not, conjuncts, to_cnf
from sympy.core.compatibility import ordered
from sympy.core.sympify import sympify
def literal_symbol(literal):
"""
The symbol in this literal (without the negation).
Examples
========
>>> from sympy.abc import A
>>> from sympy.logic.inference import literal_symbol
>>> literal_symbol(A)
A
>>> literal_symbol(~A)
A
"""
if literal is True or literal is False:
return literal
try:
if literal.is_Symbol:
return literal
if literal.is_Not:
return literal_symbol(literal.args[0])
else:
raise ValueError
except (AttributeError, ValueError):
raise ValueError("Argument must be a boolean literal.")
[docs]def satisfiable(expr, algorithm="dpll2", all_models=False):
"""
Check satisfiability of a propositional sentence.
Returns a model when it succeeds.
Returns {true: true} for trivially true expressions.
On setting all_models to True, if given expr is satisfiable then
returns a generator of models. However, if expr is unsatisfiable
then returns a generator containing the single element False.
Examples
========
>>> from sympy.abc import A, B
>>> from sympy.logic.inference import satisfiable
>>> satisfiable(A & ~B)
{A: True, B: False}
>>> satisfiable(A & ~A)
False
>>> satisfiable(True)
{True: True}
>>> next(satisfiable(A & ~A, all_models=True))
False
>>> models = satisfiable((A >> B) & B, all_models=True)
>>> next(models)
{A: False, B: True}
>>> next(models)
{A: True, B: True}
>>> def use_models(models):
... for model in models:
... if model:
... # Do something with the model.
... print(model)
... else:
... # Given expr is unsatisfiable.
... print("UNSAT")
>>> use_models(satisfiable(A >> ~A, all_models=True))
{A: False}
>>> use_models(satisfiable(A ^ A, all_models=True))
UNSAT
"""
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, all_models)
raise NotImplementedError
def valid(expr):
"""
Check validity of a propositional sentence.
A valid propositional sentence is True under every assignment.
Examples
========
>>> from sympy.abc import A, B
>>> from sympy.logic.inference import valid
>>> valid(A | ~A)
True
>>> valid(A | B)
False
References
==========
.. [1] https://en.wikipedia.org/wiki/Validity
"""
return not satisfiable(Not(expr))
def pl_true(expr, model={}, deep=False):
"""
Returns whether the given assignment is a model or not.
If the assignment does not specify the value for every proposition,
this may return None to indicate 'not obvious'.
Parameters
==========
model : dict, optional, default: {}
Mapping of symbols to boolean values to indicate assignment.
deep: boolean, optional, default: False
Gives the value of the expression under partial assignments
correctly. May still return None to indicate 'not obvious'.
Examples
========
>>> from sympy.abc import A, B, C
>>> from sympy.logic.inference import pl_true
>>> pl_true( A & B, {A: True, B: True})
True
>>> pl_true(A & B, {A: False})
False
>>> pl_true(A & B, {A: True})
>>> pl_true(A & B, {A: True}, deep=True)
>>> pl_true(A >> (B >> A))
>>> pl_true(A >> (B >> A), deep=True)
True
>>> pl_true(A & ~A)
>>> pl_true(A & ~A, deep=True)
False
>>> pl_true(A & B & (~A | ~B), {A: True})
>>> pl_true(A & B & (~A | ~B), {A: True}, deep=True)
False
"""
from sympy.core.symbol import Symbol
from sympy.logic.boolalg import BooleanFunction
boolean = (True, False)
def _validate(expr):
if isinstance(expr, Symbol) or expr in boolean:
return True
if not isinstance(expr, BooleanFunction):
return False
return all(_validate(arg) for arg in expr.args)
if expr in boolean:
return expr
expr = sympify(expr)
if not _validate(expr):
raise ValueError("%s is not a valid boolean expression" % expr)
model = dict((k, v) for k, v in model.items() if v in boolean)
result = expr.subs(model)
if result in boolean:
return bool(result)
if deep:
model = dict((k, True) for k in result.atoms())
if pl_true(result, model):
if valid(result):
return True
else:
if not satisfiable(result):
return False
return None
def entails(expr, formula_set={}):
"""
Check whether the given expr_set entail an expr.
If formula_set is empty then it returns the validity of expr.
Examples
========
>>> from sympy.abc import A, B, C
>>> from sympy.logic.inference import entails
>>> entails(A, [A >> B, B >> C])
False
>>> entails(C, [A >> B, B >> C, A])
True
>>> entails(A >> B)
False
>>> entails(A >> (B >> A))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Logical_consequence
"""
formula_set = list(formula_set)
formula_set.append(Not(expr))
return not satisfiable(And(*formula_set))
class KB(object):
"""Base class for all knowledge bases"""
def __init__(self, sentence=None):
self.clauses_ = set()
if sentence:
self.tell(sentence)
def tell(self, sentence):
raise NotImplementedError
def ask(self, query):
raise NotImplementedError
def retract(self, sentence):
raise NotImplementedError
@property
def clauses(self):
return list(ordered(self.clauses_))
class PropKB(KB):
"""A KB for Propositional Logic. Inefficient, with no indexing."""
def tell(self, sentence):
"""Add the sentence's clauses to the KB
Examples
========
>>> from sympy.logic.inference import PropKB
>>> from sympy.abc import x, y
>>> l = PropKB()
>>> l.clauses
[]
>>> l.tell(x | y)
>>> l.clauses
[x | y]
>>> l.tell(y)
>>> l.clauses
[y, x | y]
"""
for c in conjuncts(to_cnf(sentence)):
self.clauses_.add(c)
def ask(self, query):
"""Checks if the query is true given the set of clauses.
Examples
========
>>> from sympy.logic.inference import PropKB
>>> from sympy.abc import x, y
>>> l = PropKB()
>>> l.tell(x & ~y)
>>> l.ask(x)
True
>>> l.ask(y)
False
"""
return entails(query, self.clauses_)
def retract(self, sentence):
"""Remove the sentence's clauses from the KB
Examples
========
>>> from sympy.logic.inference import PropKB
>>> from sympy.abc import x, y
>>> l = PropKB()
>>> l.clauses
[]
>>> l.tell(x | y)
>>> l.clauses
[x | y]
>>> l.retract(x | y)
>>> l.clauses
[]
"""
for c in conjuncts(to_cnf(sentence)):
self.clauses_.discard(c)
