logical-agents.html (21755B)
1 <!DOCTYPE html> 2 <html> 3 <head> 4 <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> 5 <link rel="Stylesheet" type="text/css" href="style.css"> 6 <title>logical-agents</title> 7 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> 8 </head> 9 <body> 10 11 <div id="Logical agents"><h1 id="Logical agents">Logical agents</h1></div> 12 13 <div id="Logical agents-What is logic"><h2 id="What is logic">What is logic</h2></div> 14 <p> 15 logic: generic method to deal with partial/imperfect/implicit information 16 </p> 17 18 <p> 19 we need: 20 </p> 21 <ul> 22 <li> 23 syntax to write statement about rules & knowledge of the game (a language) 24 25 <li> 26 semantics to say what legal expressions mean, the meaning of each sentence with respect to interpretations 27 28 <li> 29 calculus for how to determine meaning for legal expressions 30 31 </ul> 32 33 <p> 34 knowledge-based/logical agents must be able to: 35 </p> 36 <ul> 37 <li> 38 represent states & actions 39 40 <li> 41 incorporate new percepts, update internal representation of world 42 43 <li> 44 deduce hidden properties of the world & appropriate actions 45 46 </ul> 47 48 <p> 49 online/exploratory search: go to position, evaluate all options, possibly look ahead. have to re-evaluate current position. 50 </p> 51 52 <div id="Logical agents-Syntax"><h2 id="Syntax">Syntax</h2></div> 53 <div id="Logical agents-Syntax-Propositional logic (PL)"><h3 id="Propositional logic (PL)">Propositional logic (PL)</h3></div> 54 <p> 55 assumes world contains facts 56 </p> 57 58 <p> 59 uses proposition symbols to state these facts. 60 </p> 61 62 <p> 63 pros: 64 </p> 65 <ul> 66 <li> 67 declarative 68 69 <li> 70 allows partial/disjunctive/negated information 71 72 <li> 73 is compositional 74 75 <li> 76 meaning of statements is context-independent 77 78 </ul> 79 80 <p> 81 cons: 82 </p> 83 <ul> 84 <li> 85 very limited expressive power 86 87 </ul> 88 89 <div id="Logical agents-Syntax-First order logic (FOL)"><h3 id="First order logic (FOL)">First order logic (FOL)</h3></div> 90 <p> 91 an extension of propositional logic. 92 </p> 93 94 <p> 95 allows variables to range over atomic symbols in the domain. 96 </p> 97 98 <p> 99 assumes world contains: 100 </p> 101 <ul> 102 <li> 103 objects: people, houses, colors, baseball games, etc. 104 105 <li> 106 relations: red, round, prime, brother of, comes between, bigger than, etc. 107 108 <li> 109 functions: father of, best friend, one more than, plus, etc. 110 111 </ul> 112 113 <div id="Logical agents-Syntax-First order logic (FOL)-Basic elements:"><h4 id="Basic elements:">Basic elements:</h4></div> 114 <ul> 115 <li> 116 Constants: KingJohn, 2, UCB, ... 117 118 <li> 119 Predicates: Brother, >, ... 120 121 <li> 122 Functions: Sqrt, LeftLegOf, ... 123 124 <li> 125 Variables: x, y, ... 126 127 <li> 128 Connectives: ∧, ∨, ¬, ⇒, ⇔ 129 130 </ul> 131 132 <div id="Logical agents-Syntax-First order logic (FOL)-Sentences"><h4 id="Sentences">Sentences</h4></div> 133 <pre> 134 Atomic sentence = predicate (term_1,..., term_n) 135 or term_1 = term_2 136 Term = function(term_1,..., term_n) 137 or constant 138 or variable 139 </pre> 140 141 <p> 142 Complex sentences are made from atomic sentences using connectives. 143 </p> 144 145 <div id="Logical agents-Syntax-First order logic (FOL)-Quantification"><h4 id="Quantification">Quantification</h4></div> 146 <div id="Logical agents-Syntax-First order logic (FOL)-Quantification-Universal quantification"><h5 id="Universal quantification">Universal quantification</h5></div> 147 <p> 148 ∀ <variables> <sentence> 149 </p> 150 151 <p> 152 ∀x P is true in a model <em>m</em> iff P is true with x being each possible object in the model 153 </p> 154 155 <p> 156 (you can roughly translate that to conjunctions) 157 </p> 158 159 <p> 160 typically used with ⇒ 161 </p> 162 163 <p> 164 <span id="Logical agents-Syntax-First order logic (FOL)-Quantification-Universal quantification-CARE:"></span><strong id="CARE:">CARE:</strong> ∀x ∀y ≠ ∀y ∀x 165 </p> 166 167 <div id="Logical agents-Syntax-First order logic (FOL)-Quantification-Existential quantification"><h5 id="Existential quantification">Existential quantification</h5></div> 168 <p> 169 ∃ <variables> <sentence> 170 </p> 171 172 <p> 173 ∃x P is true in a model <em>m</em> iff P is true with x being some possible object in the model 174 </p> 175 176 <p> 177 (you can roughly translate that to disjunction of instantiations of P) 178 </p> 179 180 <p> 181 typically used with ∧ 182 </p> 183 184 <p> 185 watch out, if you use it with ⇒, it works even if the LHS is false! 186 </p> 187 188 <p> 189 <span id="Logical agents-Syntax-First order logic (FOL)-Quantification-Existential quantification-CARE"></span><strong id="CARE">CARE</strong>: ∃x ∃y ≠ ∃y ∃x 190 </p> 191 192 <div id="Logical agents-Syntax-First order logic (FOL)-Quantification-Quantifier Duality"><h5 id="Quantifier Duality">Quantifier Duality</h5></div> 193 <p> 194 each quantifier can be expressed in terms of the other 195 </p> 196 197 <p> 198 e.g. these are the same: 199 </p> 200 <ul> 201 <li> 202 ∀x Likes(x, IceCream) -- "everyone likes ice cream" 203 204 <li> 205 ¬∃x ¬Likes(x, IceCream) -- "there is nobody who doesn't like ice cream" 206 207 </ul> 208 209 <div id="Logical agents-Syntax-First order logic (FOL)-Decidability vs undecidability"><h4 id="Decidability vs undecidability">Decidability vs undecidability</h4></div> 210 <p> 211 undecidability 212 </p> 213 <ul> 214 <li> 215 Turing machine can calculate everything that can be calculated 216 217 <li> 218 halting problem: \(K := { (i,x) | \text{program i halts when run on input x})\) 219 220 </ul> 221 222 <p> 223 decidability 224 </p> 225 <ul> 226 <li> 227 validity of FOL is not decidable (but semi-decidable) 228 229 <li> 230 if a theorem is logically entailed by an axiom, you can prove that it is. 231 232 <li> 233 if not, you can't necessarily prove that it's not (because you can continue with your proof infinitely). 234 235 </ul> 236 237 <div id="Logical agents-Syntax-First order logic (FOL)-Knowledge engineering in FOL"><h4 id="Knowledge engineering in FOL">Knowledge engineering in FOL</h4></div> 238 <ol> 239 <li> 240 Identify the task 241 242 <li> 243 Assemble relevant knowledge 244 245 <li> 246 Decide on vocabulary of predicates, functions, and constants 247 248 <li> 249 Encode general knowledge about the domain (terms that we want to use) 250 251 <li> 252 Encode description of the specific problem instance 253 254 <li> 255 Pose queries to the inference procedure and get answers 256 257 </ol> 258 259 <div id="Logical agents-Syntax-Choice of formalisms"><h3 id="Choice of formalisms">Choice of formalisms</h3></div> 260 <p> 261 first-order logic: represents knowledge 262 </p> 263 264 <p> 265 propositional logic: used for reasoning ("propositionalisation") 266 </p> 267 268 <p> 269 then use reasoner to check for entailment of propositional logic knowledge base an decision query 270 </p> 271 <ul> 272 <li> 273 Davis Putnam (DPLL) algorithm 274 275 <li> 276 formulas have to be in clause normal form (CNF) 277 278 <li> 279 calculus is proof by refutation: 280 281 <ul> 282 <li> 283 DPLL determines satisfiability of a KB 284 285 <li> 286 entailment of KB |= a by "refutation": 287 288 <ul> 289 <li> 290 KB |= a if KB ∩ {~a} is unsatisfiable 291 292 <li> 293 assume the opposite and prove it's impossible 294 295 </ul> 296 </ul> 297 </ul> 298 299 <div id="Logical agents-Syntax-Propositionalising FOL"><h3 id="Propositionalising FOL">Propositionalising FOL</h3></div> 300 <div id="Logical agents-Syntax-Propositionalising FOL-Reduction to propositional inference"><h4 id="Reduction to propositional inference">Reduction to propositional inference</h4></div> 301 <p> 302 every FOL KB can be propositionalised so as to preserve entailment 303 </p> 304 305 <p> 306 if a sentence α is entailed by an FOL KB, it is entailed by a <em>finite</em> subset of the propositionalised KB 307 </p> 308 309 <div id="Logical agents-Syntax-Propositionalising FOL-Universal instantiation (UI):"><h4 id="Universal instantiation (UI):">Universal instantiation (UI):</h4></div> 310 <p> 311 every instantiation of a universally quantified sentence is entailed by it. 312 </p> 313 314 <p> 315 <img src="img/univ-instant.png" alt="Universal instantiation" /> 316 </p> 317 318 <p> 319 example: 320 </p> 321 <pre> 322 ∀x King(x) ∧ Greedy(x) ⇒ Evil(x) 323 King(John) ∧ Greedy(John) ⇒ Evil(John) 324 etc. 325 </pre> 326 327 <div id="Logical agents-Syntax-Propositionalising FOL-Existential instantiation (EI):"><h4 id="Existential instantiation (EI):">Existential instantiation (EI):</h4></div> 328 <p> 329 <img src="img/exist-instant.png" alt="Existential instantiation" /> 330 </p> 331 332 <p> 333 example: 334 </p> 335 <pre> 336 ∃x Crown(x) ∧ OnHead(x,John) 337 Crown(C_1) ∧ OnHead(C_1, John) 338 </pre> 339 340 <div id="Logical agents-Syntax-Propositionalising FOL-Applying in Schnapsen - Strategies (examples)"><h4 id="Applying in Schnapsen - Strategies (examples)">Applying in Schnapsen - Strategies (examples)</h4></div> 341 <div id="Logical agents-Syntax-Propositionalising FOL-Applying in Schnapsen - Strategies (examples)-Play Jack"><h5 id="Play Jack">Play Jack</h5></div> 342 343 <p> 344 check whether card is a jack: 345 </p> 346 347 <pre> 348 KB |= PlayJack(x) ? 349 </pre> 350 351 <p> 352 represent strategy: 353 </p> 354 355 <pre> 356 ∀x PlayJack(x) ⇔ Jack(x) 357 </pre> 358 359 <p> 360 represent game information: 361 </p> 362 363 <pre> 364 KB = {Jack(4), Jack(0), Jack(14), Jack(19)} 365 </pre> 366 367 <div id="Logical agents-Syntax-Propositionalising FOL-Applying in Schnapsen - Strategies (examples)-Play cheap"><h5 id="Play cheap">Play cheap</h5></div> 368 <p> 369 only play Jacks: check whether card is cheap 370 </p> 371 372 <pre> 373 KB |= PlayCheap(x) ? 374 </pre> 375 376 <p> 377 represent strategy: 378 </p> 379 380 <pre> 381 ∀x PlayCheap(x) ⇔ Jack(x) ∨ Queen(x) ∨ King(x) 382 </pre> 383 384 <p> 385 represent game information: 386 </p> 387 388 <pre> 389 KB = {Jack(4), Jack(9), Jack(14), Jack(19), Queen(5), ...} 390 </pre> 391 392 <div id="Logical agents-Syntax-Propositionalising FOL-Applying in Schnapsen - Strategies (examples)-Play trump marriage"><h5 id="Play trump marriage">Play trump marriage</h5></div> 393 <pre> 394 TrumpMarriage(x) ⇔ Q(x) & Trump(x) & ∃y: SameColor(x,y) & K(y) & MyCard(y) 395 SameColor(x,y) ⇔ (C(x) & C(y)) ∨ (D(x) & D(y)) ∨ (H(x) & H(y)) ∨ (S(x) & S(y)) 396 </pre> 397 398 <div id="Logical agents-Semantics"><h2 id="Semantics">Semantics</h2></div> 399 <div id="Logical agents-Semantics-Interpretations & Models"><h3 id="Interpretations & Models">Interpretations & Models</h3></div> 400 <p> 401 interpretation: assignment of meaning to symbols of formal language 402 </p> 403 404 <p> 405 model: interpretation that satisfies defining axioms of knowledge base 406 </p> 407 408 <p> 409 <em>m</em> is a model of a sentence <em>α</em> if <em>α</em> holds in <em>m</em>. 410 </p> 411 412 <p> 413 M(a) is the set of all models of a. 414 </p> 415 416 <p> 417 each model specifies true/false for each proposition symbol (∧, ∨, ¬, ⇒, ⇐, ⇔) 418 </p> 419 420 <div id="Logical agents-Semantics-Entailment"><h3 id="Entailment">Entailment</h3></div> 421 <p> 422 the knowledge base (KB) entails <em>α</em>: <em>α</em> follows from the information in the knowledge base (KB |= <em>α</em>) 423 </p> 424 425 <p> 426 KB entails <em>α</em> iff <em>α</em> holds in all worlds where KB is true. 427 </p> 428 429 <p> 430 a knowledge base is the rules + observations. 431 </p> 432 433 <p> 434 a sentence is: 435 </p> 436 <ul> 437 <li> 438 entailed by KB iff α holds in all models of KB 439 440 <li> 441 valid if it is true in all models 442 443 <li> 444 satisfiable if it is true in some model 445 446 <li> 447 unsatisfiable if it is true in no models 448 449 </ul> 450 451 <p> 452 two statements are logically equivalent if they are true in same set of models: 453 </p> 454 455 <p> 456 α ≡ β iff α |= β and β |= α 457 </p> 458 459 <div id="Logical agents-Semantics-Truth"><h3 id="Truth">Truth</h3></div> 460 <p> 461 sentences are true with respect to model and interpretation. 462 </p> 463 464 <p> 465 model contains objects and relations among them 466 </p> 467 468 <p> 469 interpretation specifies referents for: 470 </p> 471 <ul> 472 <li> 473 constant symbols -- objects 474 475 <li> 476 predicate symbols -- relations 477 478 <li> 479 function symbols -- functional relations 480 481 </ul> 482 483 <p> 484 an atomic sentence \(predicate(term_1, ..., term_n)\) is true 485 iff the objects referred to by \(term_1,..., term_n\) 486 are in the relation referred to by \(predicate\) 487 </p> 488 489 <div id="Logical agents-Semantics-Validity"><h3 id="Validity">Validity</h3></div> 490 <p> 491 valid if it is true in all models. 492 </p> 493 494 <p> 495 e.g. True, A ∨ ¬A, A ⇒ A, (A ∧ (A e.g. True, A ∨ ⇒ B)) ⇒ B) 496 </p> 497 498 <div id="Logical agents-Semantics-Satisfiability"><h3 id="Satisfiability">Satisfiability</h3></div> 499 <ul> 500 <li> 501 satisfiable if it is true in <em>some</em> model 502 503 <li> 504 unsatisfiable if it is true in <em>no</em> models 505 506 </ul> 507 508 <div id="Logical agents-Calculus (algorithms for inference)"><h2 id="Calculus (algorithms for inference)">Calculus (algorithms for inference)</h2></div> 509 <div id="Logical agents-Calculus (algorithms for inference)-Properties of inference"><h3 id="Properties of inference">Properties of inference</h3></div> 510 <p> 511 sound: if an algorithm \(|-\) only derives entailed sentences. 512 i.e. if KB \(|-\) α also KB |= α 513 </p> 514 515 <p> 516 complete: if an algorithm derives any sentence that is entailed. 517 i.e. KB |= α implies KB |- α 518 </p> 519 520 <p> 521 a calculus terminates if it finds entailed sentences in finite time. 522 </p> 523 524 <p> 525 a logic is <em>decidable</em> if there is <em>sound and complete</em> calculus that <em>terminates</em>. 526 </p> 527 528 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods"><h3 id="Proof methods">Proof methods</h3></div> 529 <ol> 530 <li> 531 Model checking and search 532 533 <ul> 534 <li> 535 truth table enumeration (exponential in n) 536 537 <li> 538 improved backtracking (DPLL) 539 540 <li> 541 heuristics for choosing right order 542 543 </ul> 544 <li> 545 application of inference rules 546 547 <ul> 548 <li> 549 sound generation of new sentences from old 550 551 <li> 552 proof = sequence of rule applications (actions) 553 554 </ul> 555 </ol> 556 557 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Model checking & search"><h4 id="Model checking & search">Model checking & search</h4></div> 558 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Model checking & search-Truth Tables for inference"><h5 id="Truth Tables for inference">Truth Tables for inference</h5></div> 559 <p> 560 enumerate interpretations and check that where KB is true, α is true. 561 </p> 562 563 <table> 564 <tr> 565 <th> 566 \(fact_1\) 567 </th> 568 <th> 569 \(fact_2\) 570 </th> 571 <th> 572 \(fact_3\) 573 </th> 574 <th> 575 \(KB\) 576 </th> 577 <th> 578 \(α\) 579 </th> 580 </tr> 581 <tr> 582 <td> 583 false 584 </td> 585 <td> 586 false 587 </td> 588 <td> 589 false 590 </td> 591 <td> 592 false 593 </td> 594 <td> 595 true 596 </td> 597 </tr> 598 <tr> 599 <td> 600 false 601 </td> 602 <td> 603 false 604 </td> 605 <td> 606 false 607 </td> 608 <td> 609 false 610 </td> 611 <td> 612 true 613 </td> 614 </tr> 615 <tr> 616 <td> 617 false 618 </td> 619 <td> 620 true 621 </td> 622 <td> 623 false 624 </td> 625 <td> 626 <em>true</em> 627 </td> 628 <td> 629 <em>true</em> 630 </td> 631 </tr> 632 </table> 633 634 <p> 635 algorithm: 636 </p> 637 638 <pre> 639 for (m in truth assignments) { 640 if (m makes F true) return "satisfiable" 641 } 642 return "unsatisfiable" 643 </pre> 644 645 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Model checking & search-Effective proofs by model checking"><h5 id="Effective proofs by model checking">Effective proofs by model checking</h5></div> 646 647 <p> 648 Clever search (depth first, redundancy, heuristics) 649 </p> 650 651 <p> 652 Two families of efficient algorithms for propositional inference based on model checking 653 </p> 654 <ul> 655 <li> 656 complete backtracking search algorithms -- DPLL (Davis, Putnam, Logemann, Loveland) 657 658 <li> 659 incomplete local search algorithm (WalkSAT algorithm) 660 661 </ul> 662 663 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Model checking & search-Clause Normal Form (CNF)"><h5 id="Clause Normal Form (CNF)">Clause Normal Form (CNF)</h5></div> 664 665 <p> 666 memo technique: the C in CNF for <em>conjunction</em> normal form 667 </p> 668 669 <p> 670 A PL formula is in CNF if it is a conjunction of disjunctions of literals. 671 </p> 672 <ul> 673 <li> 674 e.g.: {{a,b}, {~a, c}, {~b, c}} 675 676 <li> 677 equivalent to (a ∨ b) ∧ (~ a ∨ c) ∧ (~ b ∨ c) 678 679 </ul> 680 681 <p> 682 calculating CNF: 683 </p> 684 <ol> 685 <li> 686 Remove implications: 687 688 <ul> 689 <li> 690 (p ⇔ q) to ((p ⇒ q) ∧ (q ⇒ p)) 691 692 <li> 693 (p → q) to (¬ p ∨ q) 694 695 </ul> 696 <li> 697 Move negations inward: 698 699 <ul> 700 <li> 701 ¬ (p ∨ q) to (¬ p ∧ ¬ q) 702 703 <li> 704 ¬ (p ∧ q) to (¬ p ∨ ¬ q) 705 706 </ul> 707 <li> 708 Move conjunctions outward: 709 710 <ul> 711 <li> 712 (r ∨ (p ∧ q)) to ((r ∨ p) ∧ (r ∨ q)) 713 714 </ul> 715 <li> 716 Split up conjunctive clauses: 717 718 <ul> 719 <li> 720 ( (p1 ∨ p2) ∧ (q1 ∨ q2) ) to (p1 ∨ p2), (q1 ∨ q2) 721 722 </ul> 723 </ol> 724 725 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Model checking & search-DPLL algorithm"><h5 id="DPLL algorithm">DPLL algorithm</h5></div> 726 727 <p> 728 when you have CNF, you can run the DPLL algorithm. determines if propositional logic sentence in CNF is satisfiable. 729 </p> 730 731 <p> 732 returns true if F is satisfiable, false otherwise. 733 </p> 734 735 <p> 736 basically assign values until contradiction, then backtrack. 737 </p> 738 739 <p> 740 Improving DPLL: 741 </p> 742 <ul> 743 <li> 744 if a literal in a disjunction clause is true, the clause is true 745 746 <li> 747 if a literal in a disjunction clause is false, the literal can be removed 748 749 <li> 750 if a clause is empty, it is false 751 752 <li> 753 a unit literal has to be true 754 755 <li> 756 a pure literal (only appears non-negated) has to be true 757 758 </ul> 759 760 <p> 761 the algorithm: 762 </p> 763 764 <pre> 765 dpll (F, literal) { 766 remove clauses containing literal 767 shorten clauses containing ¬literal 768 if (F contains no clauses) 769 return true 770 if (F contains empty clause) 771 return false 772 if (F contains a unit or pure literal) 773 return dpll(F, literal) 774 775 choose P in F 776 if (dpll(F, ¬P)) 777 return true 778 779 return dpll(F, P) 780 } 781 </pre> 782 783 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Model checking & search-DPLL algorithm-Heuristic search in DPLL"><h6 id="Heuristic search in DPLL">Heuristic search in DPLL</h6></div> 784 785 <p> 786 used in DPLL to select proposition for branching 787 </p> 788 789 <p> 790 idea: identify most constrained variable, likely to create many unit clauses 791 </p> 792 793 <p> 794 MOM's heuristic: most occurrences in clauses of minimum length 795 </p> 796 797 <p> 798 why is it better than truth table enumeration? 799 </p> 800 <ul> 801 <li> 802 early termination: clause is true if any literal is true. sentence is false if any clause is false. 803 804 <li> 805 pure symbol heuristic: always appears with the same sign in all clauses, has to be true 806 807 <li> 808 unit clause heuristic: only one literal in the clause, so it must be true 809 810 </ul> 811 812 <p> 813 proving entailment KB |= a by refutation: 814 </p> 815 <ol> 816 <li> 817 translate KB into CNF to get cnf(KB) 818 819 <li> 820 translate ~a into CNF to get cnf(~a) 821 822 <li> 823 add cnf(~a) to cnf(KB) 824 825 <li> 826 apply DPLL until either satisfiable (model is found) or unsatisfiable (search exhausted) 827 828 <li> 829 if satisfiable, not entailed. otherwise, entailed. 830 831 </ol> 832 833 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Model checking & search-Satisfiability modulo theory"><h5 id="Satisfiability modulo theory">Satisfiability modulo theory</h5></div> 834 835 <p> 836 Boolean satisfiability (SAT): is there an assignment to the \(p_1, p_2, ..., p_n\) variables such that \(\phi\) evaluates to 1? 837 </p> 838 839 <p> 840 <img src="img/boolean-satisfiability.png" alt="Boolean satisfiability diagram" /> 841 </p> 842 843 <p> 844 SAT vs SMT: 845 </p> 846 <ul> 847 <li> 848 SMT (satisfiability modulo theories) extend SAT solving by adding extensions. 849 850 <li> 851 SMT solver can solve SAT problem, but not vice-versa. 852 853 <li> 854 SMT is used in analog circuit verification, RTL, verification, and card games. 855 856 </ul> 857 858 <p> 859 SMT theories: 860 </p> 861 <ul> 862 <li> 863 real or integer arithmetic 864 865 <li> 866 equality and uninterpreted functions 867 868 <li> 869 bit vectors and arrays 870 871 <li> 872 properties: 873 874 <ul> 875 <li> 876 decidable: an effective procedure exists to determine if formula is member of theory T 877 878 <li> 879 often quantifier-free 880 881 </ul> 882 <li> 883 core theory: 884 885 <ul> 886 <li> 887 type boolean 888 889 <li> 890 constants {TRUE, FALSE} 891 892 <li> 893 functions {AND, OR, XOR, =>} 894 895 </ul> 896 <li> 897 integer theory: 898 899 <ul> 900 <li> 901 type int 902 903 <li> 904 all numerals are int constants 905 906 <li> 907 functions {+, -, x, mod, div, abs} 908 909 </ul> 910 <li> 911 reals theory: 912 913 <ul> 914 <li> 915 type real 916 917 <li> 918 functions {+, -, x, /, <, >} 919 920 <li> 921 922 923 </ul> 924 </ul> 925 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Rule-based reasoning"><h4 id="Rule-based reasoning">Rule-based reasoning</h4></div> 926 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Rule-based reasoning-Inference rules"><h5 id="Inference rules">Inference rules</h5></div> 927 <p> 928 inference rule: logical form consisting of function taking premises, analyzing their syntax, and returning one or more conclusions 929 </p> 930 931 <p> 932 Modens Ponens: \(\frac{\alpha\implies\beta,\;\alpha}{\beta}\) 933 </p> 934 935 <p> 936 And-elimination: \(\frac{\alpha\land\beta}{\alpha}\) 937 </p> 938 939 <p> 940 logical equivalences used as rules: \(\frac{\alpha\iff\beta}{(\alpha\implies\beta)\land(\beta\implies\alpha)}\) 941 </p> 942 943 <p> 944 all logical equivalence rewriting rules: 945 </p> 946 947 <p> 948 <img src="img/logical-rewriting-rules.png" alt="Rewriting rules for logic" /> 949 </p> 950 951 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Rule-based reasoning-Searching for proofs"><h5 id="Searching for proofs">Searching for proofs</h5></div> 952 <p> 953 Finding proofs is like finding solutions to search problems. 954 </p> 955 956 <p> 957 monotonicity: set of entailed sentences can only increase as info is added to the knowledge base. 958 </p> 959 <ul> 960 <li> 961 for any sentence α and β, 962 963 <li> 964 if KB |= α, then KB ∧ β |= α 965 966 </ul> 967 968 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Rule-based reasoning-Forward and backward chaining"><h5 id="Forward and backward chaining">Forward and backward chaining</h5></div> 969 <p> 970 FC is data-driven, automatic, unconscious: 971 </p> 972 <ul> 973 <li> 974 derive all facts entailed by the KB 975 976 <li> 977 may do lots of work irrelevant to the goal 978 979 </ul> 980 981 <p> 982 BC is goal-driven, appropriate for problem-solving 983 </p> 984 <ul> 985 <li> 986 specific fact entailed by the KB 987 988 <li> 989 complexity of BC can be much less than linear in size of KB 990 991 </ul> 992 993 <div id="Logical agents-Calculus (algorithms for inference)-Proof methods-Rule-based reasoning-Resolution"><h5 id="Resolution">Resolution</h5></div> 994 <p> 995 a rule is sound if its conclusion is evaluated to true whenever the premise is evaluated to true. 996 </p> 997 998 <p> 999 can be shown to be sound using truth table: 1000 </p> 1001 1002 <p> 1003 <img src="img/sound-rules-inference.png" alt="Sound rules for inference" /> 1004 </p> 1005 1006 <p> 1007 properties resolution: 1008 </p> 1009 <ul> 1010 <li> 1011 resolution rule is sound 1012 1013 <li> 1014 resolution rule is complete (on its own) for formulas in CNF 1015 1016 <li> 1017 resolution can only decide satisfiability 1018 1019 </ul> 1020 1021 <p> 1022 algorithm (again proof by refutation): 1023 </p> 1024 <ol> 1025 <li> 1026 Convert KB ∧ ¬ α into CNF 1027 1028 <li> 1029 Apply resolution rule to resulting clauses 1030 1031 <li> 1032 Continue until: 1033 1034 <ol> 1035 <li> 1036 no new clauses can be added, hence α does not entail β 1037 1038 <li> 1039 two clauses resolve to entail empty clause, hence α entails β 1040 1041 </ol> 1042 </ol> 1043 1044 </body> 1045 </html>