logical-agents.wiki (14051B)
1 = Logical agents = 2 3 == What is logic == 4 logic: generic method to deal with partial/imperfect/implicit information 5 6 we need: 7 * syntax to write statement about rules & knowledge of the game (a language) 8 * semantics to say what legal expressions mean, the meaning of each sentence with respect to interpretations 9 * calculus for how to determine meaning for legal expressions 10 11 knowledge-based/logical agents must be able to: 12 * represent states & actions 13 * incorporate new percepts, update internal representation of world 14 * deduce hidden properties of the world & appropriate actions 15 16 online/exploratory search: go to position, evaluate all options, possibly look ahead. have to re-evaluate current position. 17 18 == Syntax == 19 === Propositional logic (PL) === 20 assumes world contains facts 21 22 uses proposition symbols to state these facts. 23 24 pros: 25 * declarative 26 * allows partial/disjunctive/negated information 27 * is compositional 28 * meaning of statements is context-independent 29 30 cons: 31 * very limited expressive power 32 33 === First order logic (FOL) === 34 an extension of propositional logic. 35 36 allows variables to range over atomic symbols in the domain. 37 38 assumes world contains: 39 * objects: people, houses, colors, baseball games, etc. 40 * relations: red, round, prime, brother of, comes between, bigger than, etc. 41 * functions: father of, best friend, one more than, plus, etc. 42 43 ==== Basic elements: ==== 44 - Constants: KingJohn, 2, UCB, ... 45 - Predicates: Brother, >, ... 46 - Functions: Sqrt, LeftLegOf, ... 47 - Variables: x, y, ... 48 - Connectives: ∧, ∨, ¬, ⇒, ⇔ 49 50 ==== Sentences ==== 51 {{{ 52 Atomic sentence = predicate (term_1,..., term_n) 53 or term_1 = term_2 54 Term = function(term_1,..., term_n) 55 or constant 56 or variable 57 }}} 58 59 Complex sentences are made from atomic sentences using connectives. 60 61 ==== Quantification ==== 62 ===== Universal quantification ===== 63 ∀ <variables> <sentence> 64 65 ∀x P is true in a model _m_ iff P is true with x being each possible object in the model 66 67 (you can roughly translate that to conjunctions) 68 69 typically used with ⇒ 70 71 *CARE:* ∀x ∀y ≠ ∀y ∀x 72 73 ===== Existential quantification ===== 74 ∃ <variables> <sentence> 75 76 ∃x P is true in a model _m_ iff P is true with x being some possible object in the model 77 78 (you can roughly translate that to disjunction of instantiations of P) 79 80 typically used with ∧ 81 82 watch out, if you use it with ⇒, it works even if the LHS is false! 83 84 *CARE*: ∃x ∃y ≠ ∃y ∃x 85 86 ===== Quantifier Duality ===== 87 each quantifier can be expressed in terms of the other 88 89 e.g. these are the same: 90 * ∀x Likes(x, IceCream) -- "everyone likes ice cream" 91 * ¬∃x ¬Likes(x, IceCream) -- "there is nobody who doesn't like ice cream" 92 93 ==== Decidability vs undecidability ==== 94 undecidability 95 * Turing machine can calculate everything that can be calculated 96 * halting problem: $K := { (i,x) | \text{program i halts when run on input x})$ 97 98 decidability 99 * validity of FOL is not decidable (but semi-decidable) 100 * if a theorem is logically entailed by an axiom, you can prove that it is. 101 * if not, you can't necessarily prove that it's not (because you can continue with your proof infinitely). 102 103 ==== Knowledge engineering in FOL ==== 104 1. Identify the task 105 2. Assemble relevant knowledge 106 3. Decide on vocabulary of predicates, functions, and constants 107 4. Encode general knowledge about the domain (terms that we want to use) 108 5. Encode description of the specific problem instance 109 6. Pose queries to the inference procedure and get answers 110 111 === Choice of formalisms === 112 first-order logic: represents knowledge 113 114 propositional logic: used for reasoning ("propositionalisation") 115 116 then use reasoner to check for entailment of propositional logic knowledge base an decision query 117 * Davis Putnam (DPLL) algorithm 118 * formulas have to be in clause normal form (CNF) 119 * calculus is proof by refutation: 120 * DPLL determines satisfiability of a KB 121 * entailment of KB |= a by "refutation": 122 * KB |= a if KB ∩ {~a} is unsatisfiable 123 * assume the opposite and prove it's impossible 124 125 === Propositionalising FOL === 126 ==== Reduction to propositional inference ==== 127 every FOL KB can be propositionalised so as to preserve entailment 128 129 if a sentence α is entailed by an FOL KB, it is entailed by a _finite_ subset of the propositionalised KB 130 131 ==== Universal instantiation (UI): ==== 132 every instantiation of a universally quantified sentence is entailed by it. 133 134 {{file:img/univ-instant.png|Universal instantiation}} 135 136 example: 137 {{{ 138 ∀x King(x) ∧ Greedy(x) ⇒ Evil(x) 139 King(John) ∧ Greedy(John) ⇒ Evil(John) 140 etc. 141 }}} 142 143 ==== Existential instantiation (EI): ==== 144 {{file:img/exist-instant.png|Existential instantiation}} 145 146 example: 147 {{{ 148 ∃x Crown(x) ∧ OnHead(x,John) 149 Crown(C_1) ∧ OnHead(C_1, John) 150 }}} 151 152 ==== Applying in Schnapsen - Strategies (examples) ==== 153 ===== Play Jack ===== 154 155 check whether card is a jack: 156 157 {{{ 158 KB |= PlayJack(x) ? 159 }}} 160 161 represent strategy: 162 163 {{{ 164 ∀x PlayJack(x) ⇔ Jack(x) 165 }}} 166 167 represent game information: 168 169 {{{ 170 KB = {Jack(4), Jack(0), Jack(14), Jack(19)} 171 }}} 172 173 ===== Play cheap ===== 174 only play Jacks: check whether card is cheap 175 176 {{{ 177 KB |= PlayCheap(x) ? 178 }}} 179 180 represent strategy: 181 182 {{{ 183 ∀x PlayCheap(x) ⇔ Jack(x) ∨ Queen(x) ∨ King(x) 184 }}} 185 186 represent game information: 187 188 {{{ 189 KB = {Jack(4), Jack(9), Jack(14), Jack(19), Queen(5), ...} 190 }}} 191 192 ===== Play trump marriage ===== 193 {{{ 194 TrumpMarriage(x) ⇔ Q(x) & Trump(x) & ∃y: SameColor(x,y) & K(y) & MyCard(y) 195 SameColor(x,y) ⇔ (C(x) & C(y)) ∨ (D(x) & D(y)) ∨ (H(x) & H(y)) ∨ (S(x) & S(y)) 196 }}} 197 198 == Semantics == 199 === Interpretations & Models === 200 interpretation: assignment of meaning to symbols of formal language 201 202 model: interpretation that satisfies defining axioms of knowledge base 203 204 _m_ is a model of a sentence _α_ if _α_ holds in _m_. 205 206 M(a) is the set of all models of a. 207 208 each model specifies true/false for each proposition symbol (∧, ∨, ¬, ⇒, ⇐, ⇔) 209 210 === Entailment === 211 the knowledge base (KB) entails _α_: _α_ follows from the information in the knowledge base (KB |= _α_) 212 213 KB entails _α_ iff _α_ holds in all worlds where KB is true. 214 215 a knowledge base is the rules + observations. 216 217 a sentence is: 218 * entailed by KB iff α holds in all models of KB 219 * valid if it is true in all models 220 * satisfiable if it is true in some model 221 * unsatisfiable if it is true in no models 222 223 two statements are logically equivalent if they are true in same set of models: 224 225 α ≡ β iff α |= β and β |= α 226 227 === Truth === 228 sentences are true with respect to model and interpretation. 229 230 model contains objects and relations among them 231 232 interpretation specifies referents for: 233 * constant symbols -- objects 234 * predicate symbols -- relations 235 * function symbols -- functional relations 236 237 an atomic sentence $predicate(term_1, ..., term_n)$ is true 238 iff the objects referred to by $term_1,..., term_n$ 239 are in the relation referred to by $predicate$ 240 241 === Validity === 242 valid if it is true in all models. 243 244 e.g. True, A ∨ ¬A, A ⇒ A, (A ∧ (A e.g. True, A ∨ ⇒ B)) ⇒ B) 245 246 === Satisfiability === 247 - satisfiable if it is true in _some_ model 248 - unsatisfiable if it is true in _no_ models 249 250 == Calculus (algorithms for inference) == 251 === Properties of inference === 252 sound: if an algorithm $|-$ only derives entailed sentences. 253 i.e. if KB $|-$ α also KB |= α 254 255 complete: if an algorithm derives any sentence that is entailed. 256 i.e. KB |= α implies KB |- α 257 258 a calculus terminates if it finds entailed sentences in finite time. 259 260 a logic is _decidable_ if there is _sound and complete_ calculus that _terminates_. 261 262 === Proof methods === 263 1. Model checking and search 264 * truth table enumeration (exponential in n) 265 * improved backtracking (DPLL) 266 * heuristics for choosing right order 267 2. application of inference rules 268 * sound generation of new sentences from old 269 * proof = sequence of rule applications (actions) 270 271 ==== Model checking & search ==== 272 ===== Truth Tables for inference ===== 273 enumerate interpretations and check that where KB is true, α is true. 274 275 | $fact_1$ | $fact_2$ | $fact_3$ | $KB$ | $α$ | 276 |----------|----------|----------|--------|--------| 277 | false | false | false | false | true | 278 | false | false | false | false | true | 279 | false | true | false | _true_ | _true_ | 280 281 algorithm: 282 283 {{{ 284 for (m in truth assignments) { 285 if (m makes F true) return "satisfiable" 286 } 287 return "unsatisfiable" 288 }}} 289 290 ===== Effective proofs by model checking ===== 291 292 Clever search (depth first, redundancy, heuristics) 293 294 Two families of efficient algorithms for propositional inference based on model checking 295 * complete backtracking search algorithms -- DPLL (Davis, Putnam, Logemann, Loveland) 296 * incomplete local search algorithm (WalkSAT algorithm) 297 298 ===== Clause Normal Form (CNF) ===== 299 300 memo technique: the C in CNF for _conjunction_ normal form 301 302 A PL formula is in CNF if it is a conjunction of disjunctions of literals. 303 * e.g.: {{a,b}, {~a, c}, {~b, c}} 304 * equivalent to (a ∨ b) ∧ (~ a ∨ c) ∧ (~ b ∨ c) 305 306 calculating CNF: 307 1. Remove implications: 308 * (p ⇔ q) to ((p ⇒ q) ∧ (q ⇒ p)) 309 * (p → q) to (¬ p ∨ q) 310 2. Move negations inward: 311 * ¬ (p ∨ q) to (¬ p ∧ ¬ q) 312 * ¬ (p ∧ q) to (¬ p ∨ ¬ q) 313 3. Move conjunctions outward: 314 * (r ∨ (p ∧ q)) to ((r ∨ p) ∧ (r ∨ q)) 315 4. Split up conjunctive clauses: 316 * ( (p1 ∨ p2) ∧ (q1 ∨ q2) ) to (p1 ∨ p2), (q1 ∨ q2) 317 318 ===== DPLL algorithm ===== 319 320 when you have CNF, you can run the DPLL algorithm. determines if propositional logic sentence in CNF is satisfiable. 321 322 returns true if F is satisfiable, false otherwise. 323 324 basically assign values until contradiction, then backtrack. 325 326 Improving DPLL: 327 * if a literal in a disjunction clause is true, the clause is true 328 * if a literal in a disjunction clause is false, the literal can be removed 329 * if a clause is empty, it is false 330 * a unit literal has to be true 331 * a pure literal (only appears non-negated) has to be true 332 333 the algorithm: 334 335 {{{ 336 dpll (F, literal) { 337 remove clauses containing literal 338 shorten clauses containing ¬literal 339 if (F contains no clauses) 340 return true 341 if (F contains empty clause) 342 return false 343 if (F contains a unit or pure literal) 344 return dpll(F, literal) 345 346 choose P in F 347 if (dpll(F, ¬P)) 348 return true 349 350 return dpll(F, P) 351 } 352 }}} 353 354 ====== Heuristic search in DPLL ====== 355 356 used in DPLL to select proposition for branching 357 358 idea: identify most constrained variable, likely to create many unit clauses 359 360 MOM's heuristic: most occurrences in clauses of minimum length 361 362 why is it better than truth table enumeration? 363 * early termination: clause is true if any literal is true. sentence is false if any clause is false. 364 * pure symbol heuristic: always appears with the same sign in all clauses, has to be true 365 * unit clause heuristic: only one literal in the clause, so it must be true 366 367 proving entailment KB |= a by refutation: 368 1. translate KB into CNF to get cnf(KB) 369 2. translate ~a into CNF to get cnf(~a) 370 3. add cnf(~a) to cnf(KB) 371 4. apply DPLL until either satisfiable (model is found) or unsatisfiable (search exhausted) 372 5. if satisfiable, not entailed. otherwise, entailed. 373 374 ===== Satisfiability modulo theory ===== 375 376 Boolean satisfiability (SAT): is there an assignment to the $p_1, p_2, ..., p_n$ variables such that $\phi$ evaluates to 1? 377 378 {{file:img/boolean-satisfiability.png|Boolean satisfiability diagram}} 379 380 SAT vs SMT: 381 * SMT (satisfiability modulo theories) extend SAT solving by adding extensions. 382 * SMT solver can solve SAT problem, but not vice-versa. 383 * SMT is used in analog circuit verification, RTL, verification, and card games. 384 385 SMT theories: 386 * real or integer arithmetic 387 * equality and uninterpreted functions 388 * bit vectors and arrays 389 * properties: 390 * decidable: an effective procedure exists to determine if formula is member of theory T 391 * often quantifier-free 392 * core theory: 393 * type boolean 394 * constants {TRUE, FALSE} 395 * functions {AND, OR, XOR, =>} 396 * integer theory: 397 * type int 398 * all numerals are int constants 399 * functions {+, -, x, mod, div, abs} 400 * reals theory: 401 * type real 402 * functions {+, -, x, /, <, >} 403 * 404 ==== Rule-based reasoning==== 405 ===== Inference rules ===== 406 inference rule: logical form consisting of function taking premises, analyzing their syntax, and returning one or more conclusions 407 408 Modens Ponens: $\frac{\alpha\implies\beta,\;\alpha}{\beta}$ 409 410 And-elimination: $\frac{\alpha\land\beta}{\alpha}$ 411 412 logical equivalences used as rules: $\frac{\alpha\iff\beta}{(\alpha\implies\beta)\land(\beta\implies\alpha)}$ 413 414 all logical equivalence rewriting rules: 415 416 {{file:img/logical-rewriting-rules.png|Rewriting rules for logic}} 417 418 ===== Searching for proofs ===== 419 Finding proofs is like finding solutions to search problems. 420 421 monotonicity: set of entailed sentences can only increase as info is added to the knowledge base. 422 * for any sentence α and β, 423 * if KB |= α, then KB ∧ β |= α 424 425 ===== Forward and backward chaining ===== 426 FC is data-driven, automatic, unconscious: 427 * derive all facts entailed by the KB 428 * may do lots of work irrelevant to the goal 429 430 BC is goal-driven, appropriate for problem-solving 431 * specific fact entailed by the KB 432 * complexity of BC can be much less than linear in size of KB 433 434 ===== Resolution ===== 435 a rule is sound if its conclusion is evaluated to true whenever the premise is evaluated to true. 436 437 can be shown to be sound using truth table: 438 439 {{file:img/sound-rules-inference.png|Sound rules for inference}} 440 441 properties resolution: 442 * resolution rule is sound 443 * resolution rule is complete (on its own) for formulas in CNF 444 * resolution can only decide satisfiability 445 446 algorithm (again proof by refutation): 447 1. Convert KB ∧ ¬ α into CNF 448 2. Apply resolution rule to resulting clauses 449 3. Continue until: 450 a) no new clauses can be added, hence α does not entail β 451 b) two clauses resolve to entail empty clause, hence α entails β 452