1"""Inference in propositional logic""" 2 3from ..core.sympify import sympify 4from ..utilities import ordered 5from .boolalg import And, Not, conjuncts, to_cnf 6 7 8def literal_symbol(literal): 9 """ 10 The symbol in this literal (without the negation). 11 12 Examples 13 ======== 14 15 >>> literal_symbol(a) 16 a 17 >>> literal_symbol(~a) 18 a 19 20 """ 21 if literal is True or literal is False: 22 return literal 23 try: 24 if literal.is_Symbol: 25 return literal 26 if literal.is_Not: 27 return literal_symbol(literal.args[0]) 28 else: 29 raise ValueError 30 except (AttributeError, ValueError): 31 raise ValueError('Argument must be a boolean literal.') 32 33 34def satisfiable(expr, algorithm='dpll2', all_models=False): 35 """ 36 Check satisfiability of a propositional sentence. 37 Returns a model when it succeeds. 38 Returns {true: true} for trivially true expressions. 39 40 On setting all_models to True, if given expr is satisfiable then 41 returns a generator of models. However, if expr is unsatisfiable 42 then returns a generator containing the single element False. 43 44 Examples 45 ======== 46 47 >>> satisfiable(a & ~b) 48 {a: True, b: False} 49 >>> satisfiable(a & ~a) 50 False 51 >>> satisfiable(True) 52 {true: True} 53 >>> next(satisfiable(a & ~a, all_models=True)) 54 False 55 >>> models = satisfiable((a >> b) & b, all_models=True) 56 >>> next(models) 57 {a: False, b: True} 58 >>> next(models) 59 {a: True, b: True} 60 >>> def use_models(models): 61 ... for model in models: 62 ... if model: 63 ... # Do something with the model. 64 ... return model 65 ... else: 66 ... # Given expr is unsatisfiable. 67 ... print('UNSAT') 68 >>> use_models(satisfiable(a >> ~a, all_models=True)) 69 {a: False} 70 >>> use_models(satisfiable(a ^ a, all_models=True)) 71 UNSAT 72 73 """ 74 expr = to_cnf(expr) 75 if algorithm == 'dpll': 76 from .algorithms.dpll import dpll_satisfiable 77 return dpll_satisfiable(expr) 78 elif algorithm == 'dpll2': 79 from .algorithms.dpll2 import dpll_satisfiable 80 return dpll_satisfiable(expr, all_models) 81 else: 82 raise NotImplementedError 83 84 85def valid(expr): 86 """ 87 Check validity of a propositional sentence. 88 A valid propositional sentence is True under every assignment. 89 90 Examples 91 ======== 92 93 >>> valid(a | ~a) 94 True 95 >>> valid(a | b) 96 False 97 98 References 99 ========== 100 101 * https://en.wikipedia.org/wiki/Validity 102 103 """ 104 return not satisfiable(Not(expr)) 105 106 107def pl_true(expr, model={}, deep=False): 108 """ 109 Returns whether the given assignment is a model or not. 110 111 If the assignment does not specify the value for every proposition, 112 this may return None to indicate 'not obvious'. 113 114 Parameters 115 ========== 116 117 model : dict, optional, default: {} 118 Mapping of symbols to boolean values to indicate assignment. 119 deep: boolean, optional, default: False 120 Gives the value of the expression under partial assignments 121 correctly. May still return None to indicate 'not obvious'. 122 123 124 Examples 125 ======== 126 127 >>> pl_true(a & b, {a: True, b: True}) 128 True 129 >>> pl_true(a & b, {a: False}) 130 False 131 >>> pl_true(a & b, {a: True}) 132 >>> pl_true(a & b, {a: True}, deep=True) 133 >>> pl_true(a >> (b >> a)) 134 >>> pl_true(a >> (b >> a), deep=True) 135 True 136 >>> pl_true(a & ~a) 137 >>> pl_true(a & ~a, deep=True) 138 False 139 >>> pl_true(a & b & (~a | ~b), {a: True}) 140 >>> pl_true(a & b & (~a | ~b), {a: True}, deep=True) 141 False 142 143 """ 144 from ..core import Symbol 145 from .boolalg import BooleanFunction 146 boolean = (True, False) 147 148 def _validate(expr): 149 if isinstance(expr, Symbol) or expr in boolean: 150 return True 151 if not isinstance(expr, BooleanFunction): 152 return False 153 return all(_validate(arg) for arg in expr.args) 154 155 if expr in boolean: 156 return expr 157 expr = sympify(expr) 158 if not _validate(expr): 159 raise ValueError(f'{expr} is not a valid boolean expression') 160 model = {k: v for k, v in model.items() if v in boolean} 161 result = expr.subs(model) 162 if result in boolean: 163 return bool(result) 164 if deep: 165 model = {k: True for k in result.atoms()} 166 if pl_true(result, model): 167 if valid(result): 168 return True 169 else: 170 if not satisfiable(result): 171 return False 172 173 174def entails(expr, formula_set={}): 175 """ 176 Check whether the given expr_set entail an expr. 177 If formula_set is empty then it returns the validity of expr. 178 179 Examples 180 ======== 181 182 >>> entails(a, [a >> b, b >> c]) 183 False 184 >>> entails(c, [a >> b, b >> c, a]) 185 True 186 >>> entails(a >> b) 187 False 188 >>> entails(a >> (b >> a)) 189 True 190 191 References 192 ========== 193 194 * https://en.wikipedia.org/wiki/Logical_consequence 195 196 """ 197 formula_set = list(formula_set) 198 formula_set.append(Not(expr)) 199 return not satisfiable(And(*formula_set)) 200 201 202class KB: 203 """Base class for all knowledge bases.""" 204 205 def __init__(self, sentence=None): 206 self.clauses_ = set() 207 if sentence: 208 self.tell(sentence) 209 210 def tell(self, sentence): 211 raise NotImplementedError 212 213 def ask(self, query): 214 raise NotImplementedError 215 216 def retract(self, sentence): 217 raise NotImplementedError 218 219 @property 220 def clauses(self): 221 return list(ordered(self.clauses_)) 222 223 224class PropKB(KB): 225 """A KB for Propositional Logic. Inefficient, with no indexing.""" 226 227 def tell(self, sentence): 228 """Add the sentence's clauses to the KB 229 230 Examples 231 ======== 232 233 >>> l = PropKB() 234 >>> l.clauses 235 [] 236 237 >>> l.tell(x | y) 238 >>> l.clauses 239 [x | y] 240 241 >>> l.tell(y) 242 >>> l.clauses 243 [y, x | y] 244 245 """ 246 for c in conjuncts(to_cnf(sentence)): 247 self.clauses_.add(c) 248 249 def ask(self, query): 250 """Checks if the query is true given the set of clauses. 251 252 Examples 253 ======== 254 255 >>> l = PropKB() 256 >>> l.tell(x & ~y) 257 >>> l.ask(x) 258 True 259 >>> l.ask(y) 260 False 261 262 """ 263 return entails(query, self.clauses_) 264 265 def retract(self, sentence): 266 """Remove the sentence's clauses from the KB 267 268 Examples 269 ======== 270 271 >>> l = PropKB() 272 >>> l.clauses 273 [] 274 275 >>> l.tell(x | y) 276 >>> l.clauses 277 [x | y] 278 279 >>> l.retract(x | y) 280 >>> l.clauses 281 [] 282 283 """ 284 for c in conjuncts(to_cnf(sentence)): 285 self.clauses_.discard(c) 286