Skip to content

Commit 6c7920e

Browse files
dsawantmarakis
dsaw
authored and
antmarakis
committed
Grammar and typo fixes in logic notebook (#1002)
1 parent fb9b85a commit 6c7920e

File tree

1 file changed

+77
-32
lines changed

1 file changed

+77
-32
lines changed

Diff for: ‎logic.ipynb

+77-32
Original file line numberDiff line numberDiff line change
@@ -13,15 +13,17 @@
1313
"cell_type": "markdown",
1414
"metadata": {},
1515
"source": [
16-
"This Jupyter notebook acts as supporting material for topics covered in __Chapter 6 Logical Agents__, __Chapter 7 First-Order Logic__ and __Chapter 8 Inference in First-Order Logic__ of the book *[Artificial Intelligence: A Modern Approach](http://aima.cs.berkeley.edu)*. We make use the implementations in the [logic.py](https://github.com/aimacode/aima-python/blob/master/logic.py) module. See the [intro notebook](https://github.com/aimacode/aima-python/blob/master/intro.ipynb) for instructions.\n",
16+
"This Jupyter notebook acts as supporting material for topics covered in __Chapter 6 Logical Agents__, __Chapter 7 First-Order Logic__ and __Chapter 8 Inference in First-Order Logic__ of the book *[Artificial Intelligence: A Modern Approach](http://aima.cs.berkeley.edu)*. We make use of the implementations in the [logic.py](https://github.com/aimacode/aima-python/blob/master/logic.py) module. See the [intro notebook](https://github.com/aimacode/aima-python/blob/master/intro.ipynb) for instructions.\n",
1717
"\n",
1818
"Let's first import everything from the `logic` module."
1919
]
2020
},
2121
{
2222
"cell_type": "code",
2323
"execution_count": 1,
24-
"metadata": {},
24+
"metadata": {
25+
"collapsed": true
26+
},
2527
"outputs": [],
2628
"source": [
2729
"from utils import *\n",
@@ -98,7 +100,9 @@
98100
{
99101
"cell_type": "code",
100102
"execution_count": 3,
101-
"metadata": {},
103+
"metadata": {
104+
"collapsed": true
105+
},
102106
"outputs": [],
103107
"source": [
104108
"(x, y, P, Q, f) = symbols('x, y, P, Q, f')"
@@ -426,7 +430,9 @@
426430
{
427431
"cell_type": "code",
428432
"execution_count": 15,
429-
"metadata": {},
433+
"metadata": {
434+
"collapsed": true
435+
},
430436
"outputs": [],
431437
"source": [
432438
"wumpus_kb = PropKB()"
@@ -444,7 +450,9 @@
444450
{
445451
"cell_type": "code",
446452
"execution_count": 16,
447-
"metadata": {},
453+
"metadata": {
454+
"collapsed": true
455+
},
448456
"outputs": [],
449457
"source": [
450458
"P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21')"
@@ -461,7 +469,9 @@
461469
{
462470
"cell_type": "code",
463471
"execution_count": 17,
464-
"metadata": {},
472+
"metadata": {
473+
"collapsed": true
474+
},
465475
"outputs": [],
466476
"source": [
467477
"wumpus_kb.tell(~P11)"
@@ -477,7 +487,9 @@
477487
{
478488
"cell_type": "code",
479489
"execution_count": 18,
480-
"metadata": {},
490+
"metadata": {
491+
"collapsed": true
492+
},
481493
"outputs": [],
482494
"source": [
483495
"wumpus_kb.tell(B11 | '<=>' | ((P12 | P21)))\n",
@@ -494,7 +506,9 @@
494506
{
495507
"cell_type": "code",
496508
"execution_count": 19,
497-
"metadata": {},
509+
"metadata": {
510+
"collapsed": true
511+
},
498512
"outputs": [],
499513
"source": [
500514
"wumpus_kb.tell(~B11)\n",
@@ -564,7 +578,7 @@
564578
"<br>\n",
565579
"The purpose of a KB agent is to provide a level of abstraction over knowledge-base manipulation and is to be used as a base class for agents that work on a knowledge base.\n",
566580
"<br>\n",
567-
"Given a percept, the KB agent adds the percept to its knowledge base, asks the knowledge base for the best action, and tells the knowledge base that it has infact taken that action.\n",
581+
"Given a percept, the KB agent adds the percept to its knowledge base, asks the knowledge base for the best action, and tells the knowledge base that it has in fact taken that action.\n",
568582
"<br>\n",
569583
"Our implementation of `KB-Agent` is encapsulated in a class `KB_AgentProgram` which inherits from the `KB` class.\n",
570584
"<br>\n",
@@ -1168,7 +1182,7 @@
11681182
"source": [
11691183
"### Proof by Resolution\n",
11701184
"Recall that our goal is to check whether $\\text{KB} \\vDash \\alpha$ i.e. is $\\text{KB} \\implies \\alpha$ true in every model. Suppose we wanted to check if $P \\implies Q$ is valid. We check the satisfiability of $\\neg (P \\implies Q)$, which can be rewritten as $P \\land \\neg Q$. If $P \\land \\neg Q$ is unsatisfiable, then $P \\implies Q$ must be true in all models. This gives us the result \"$\\text{KB} \\vDash \\alpha$ <em>if and only if</em> $\\text{KB} \\land \\neg \\alpha$ is unsatisfiable\".<br/>\n",
1171-
"This technique corresponds to <em>proof by <strong>contradiction</strong></em>, a standard mathematical proof technique. We assume $\\alpha$ to be false and show that this leads to a contradiction with known axioms in $\\text{KB}$. We obtain a contradiction by making valid inferences using inference rules. In this proof we use a single inference rule, <strong>resolution</strong> which states $(l_1 \\lor \\dots \\lor l_k) \\land (m_1 \\lor \\dots \\lor m_n) \\land (l_i \\iff \\neg m_j) \\implies l_1 \\lor \\dots \\lor l_{i - 1} \\lor l_{i + 1} \\lor \\dots \\lor l_k \\lor m_1 \\lor \\dots \\lor m_{j - 1} \\lor m_{j + 1} \\lor \\dots \\lor m_n$. Applying the resolution yeilds us a clause which we add to the KB. We keep doing this until:\n",
1185+
"This technique corresponds to <em>proof by <strong>contradiction</strong></em>, a standard mathematical proof technique. We assume $\\alpha$ to be false and show that this leads to a contradiction with known axioms in $\\text{KB}$. We obtain a contradiction by making valid inferences using inference rules. In this proof we use a single inference rule, <strong>resolution</strong> which states $(l_1 \\lor \\dots \\lor l_k) \\land (m_1 \\lor \\dots \\lor m_n) \\land (l_i \\iff \\neg m_j) \\implies l_1 \\lor \\dots \\lor l_{i - 1} \\lor l_{i + 1} \\lor \\dots \\lor l_k \\lor m_1 \\lor \\dots \\lor m_{j - 1} \\lor m_{j + 1} \\lor \\dots \\lor m_n$. Applying the resolution yields us a clause which we add to the KB. We keep doing this until:\n",
11721186
"\n",
11731187
"* There are no new clauses that can be added, in which case $\\text{KB} \\nvDash \\alpha$.\n",
11741188
"* Two clauses resolve to yield the <em>empty clause</em>, in which case $\\text{KB} \\vDash \\alpha$.\n",
@@ -2009,10 +2023,9 @@
20092023
"metadata": {},
20102024
"source": [
20112025
"### Forward and backward chaining\n",
2012-
"Previously, we said we will look at two algorithms to check if a sentence is entailed by the `KB`, \n",
2013-
"but here's a third one. \n",
2026+
"Previously, we said we will look at two algorithms to check if a sentence is entailed by the `KB`. Here's a third one. \n",
20142027
"The difference here is that our goal now is to determine if a knowledge base of definite clauses entails a single proposition symbol *q* - the query.\n",
2015-
"There is a catch however, the knowledge base can only contain **Horn clauses**.\n",
2028+
"There is a catch however - the knowledge base can only contain **Horn clauses**.\n",
20162029
"<br>\n",
20172030
"#### Horn Clauses\n",
20182031
"Horn clauses can be defined as a *disjunction* of *literals* with **at most** one positive literal. \n",
@@ -2346,7 +2359,9 @@
23462359
{
23472360
"cell_type": "code",
23482361
"execution_count": 41,
2349-
"metadata": {},
2362+
"metadata": {
2363+
"collapsed": true
2364+
},
23502365
"outputs": [],
23512366
"source": [
23522367
"clauses = ['(B & F)==>E', \n",
@@ -2370,7 +2385,9 @@
23702385
{
23712386
"cell_type": "code",
23722387
"execution_count": 42,
2373-
"metadata": {},
2388+
"metadata": {
2389+
"collapsed": true
2390+
},
23742391
"outputs": [],
23752392
"source": [
23762393
"definite_clauses_KB = PropDefiniteKB()\n",
@@ -2800,7 +2817,9 @@
28002817
{
28012818
"cell_type": "code",
28022819
"execution_count": 49,
2803-
"metadata": {},
2820+
"metadata": {
2821+
"collapsed": true
2822+
},
28042823
"outputs": [],
28052824
"source": [
28062825
"A, B, C, D = expr('A, B, C, D')"
@@ -2932,7 +2951,7 @@
29322951
"This is similar to finding a neighboring state in the `hill_climbing` algorithm.\n",
29332952
"<br>\n",
29342953
"The symbol to be flipped is decided by an evaluation function that counts the number of unsatisfied clauses.\n",
2935-
"Sometimes, symbols are also flipped randomly, to avoid local optima. A subtle balance between greediness and randomness is required. Alternatively, some versions of the algorithm restart with a completely new random assignment if no solution has been found for too long, as a way of getting out of local minima of numbers of unsatisfied clauses.\n",
2954+
"Sometimes, symbols are also flipped randomly to avoid local optima. A subtle balance between greediness and randomness is required. Alternatively, some versions of the algorithm restart with a completely new random assignment if no solution has been found for too long as a way of getting out of local minima of numbers of unsatisfied clauses.\n",
29362955
"<br>\n",
29372956
"<br>\n",
29382957
"Let's have a look at the algorithm."
@@ -3097,7 +3116,9 @@
30973116
{
30983117
"cell_type": "code",
30993118
"execution_count": 56,
3100-
"metadata": {},
3119+
"metadata": {
3120+
"collapsed": true
3121+
},
31013122
"outputs": [],
31023123
"source": [
31033124
"A, B, C, D = expr('A, B, C, D')"
@@ -3173,7 +3194,9 @@
31733194
{
31743195
"cell_type": "code",
31753196
"execution_count": 60,
3176-
"metadata": {},
3197+
"metadata": {
3198+
"collapsed": true
3199+
},
31773200
"outputs": [],
31783201
"source": [
31793202
"WalkSAT([A & B, C | D, ~(D | B)], 0.5, 1000)"
@@ -3198,7 +3221,9 @@
31983221
{
31993222
"cell_type": "code",
32003223
"execution_count": 61,
3201-
"metadata": {},
3224+
"metadata": {
3225+
"collapsed": true
3226+
},
32023227
"outputs": [],
32033228
"source": [
32043229
"def WalkSAT_CNF(sentence, p=0.5, max_flips=10000):\n",
@@ -3248,7 +3273,9 @@
32483273
{
32493274
"cell_type": "code",
32503275
"execution_count": 63,
3251-
"metadata": {},
3276+
"metadata": {
3277+
"collapsed": true
3278+
},
32523279
"outputs": [],
32533280
"source": [
32543281
"sentence_1 = A |'<=>'| B\n",
@@ -3602,7 +3629,9 @@
36023629
{
36033630
"cell_type": "code",
36043631
"execution_count": 69,
3605-
"metadata": {},
3632+
"metadata": {
3633+
"collapsed": true
3634+
},
36063635
"outputs": [],
36073636
"source": [
36083637
"clauses = []"
@@ -3629,7 +3658,9 @@
36293658
{
36303659
"cell_type": "code",
36313660
"execution_count": 70,
3632-
"metadata": {},
3661+
"metadata": {
3662+
"collapsed": true
3663+
},
36333664
"outputs": [],
36343665
"source": [
36353666
"clauses.append(expr(\"(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)\"))"
@@ -3648,7 +3679,9 @@
36483679
{
36493680
"cell_type": "code",
36503681
"execution_count": 71,
3651-
"metadata": {},
3682+
"metadata": {
3683+
"collapsed": true
3684+
},
36523685
"outputs": [],
36533686
"source": [
36543687
"clauses.append(expr(\"Enemy(Nono, America)\"))"
@@ -3667,7 +3700,9 @@
36673700
{
36683701
"cell_type": "code",
36693702
"execution_count": 72,
3670-
"metadata": {},
3703+
"metadata": {
3704+
"collapsed": true
3705+
},
36713706
"outputs": [],
36723707
"source": [
36733708
"clauses.append(expr(\"Owns(Nono, M1)\"))\n",
@@ -3689,7 +3724,9 @@
36893724
{
36903725
"cell_type": "code",
36913726
"execution_count": 73,
3692-
"metadata": {},
3727+
"metadata": {
3728+
"collapsed": true
3729+
},
36933730
"outputs": [],
36943731
"source": [
36953732
"clauses.append(expr(\"(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)\"))"
@@ -3708,7 +3745,9 @@
37083745
{
37093746
"cell_type": "code",
37103747
"execution_count": 74,
3711-
"metadata": {},
3748+
"metadata": {
3749+
"collapsed": true
3750+
},
37123751
"outputs": [],
37133752
"source": [
37143753
"clauses.append(expr(\"American(West)\"))"
@@ -3726,7 +3765,9 @@
37263765
{
37273766
"cell_type": "code",
37283767
"execution_count": 75,
3729-
"metadata": {},
3768+
"metadata": {
3769+
"collapsed": true
3770+
},
37303771
"outputs": [],
37313772
"source": [
37323773
"clauses.append(expr(\"Missile(x) ==> Weapon(x)\"))\n",
@@ -3743,7 +3784,9 @@
37433784
{
37443785
"cell_type": "code",
37453786
"execution_count": 76,
3746-
"metadata": {},
3787+
"metadata": {
3788+
"collapsed": true
3789+
},
37473790
"outputs": [],
37483791
"source": [
37493792
"crime_kb = FolKB(clauses)"
@@ -4039,7 +4082,7 @@
40394082
"metadata": {},
40404083
"source": [
40414084
"### Forward Chaining Algorithm\n",
4042-
"We consider the simple forward-chaining algorithm presented in <em>Figure 9.3</em>. We look at each rule in the knoweldge base and see if the premises can be satisfied. This is done by finding a substitution which unifies each of the premise with a clause in the `KB`. If we are able to unify the premises, the conclusion (with the corresponding substitution) is added to the `KB`. This inferencing process is repeated until either the query can be answered or till no new sentences can be added. We test if the newly added clause unifies with the query in which case the substitution yielded by `unify` is an answer to the query. If we run out of sentences to infer, this means the query was a failure.\n",
4085+
"We consider the simple forward-chaining algorithm presented in <em>Figure 9.3</em>. We look at each rule in the knowledge base and see if the premises can be satisfied. This is done by finding a substitution which unifies each of the premise with a clause in the `KB`. If we are able to unify the premises, the conclusion (with the corresponding substitution) is added to the `KB`. This inferencing process is repeated until either the query can be answered or till no new sentences can be added. We test if the newly added clause unifies with the query in which case the substitution yielded by `unify` is an answer to the query. If we run out of sentences to infer, this means the query was a failure.\n",
40434086
"\n",
40444087
"The function `fol_fc_ask` is a generator which yields all substitutions which validate the query."
40454088
]
@@ -4514,7 +4557,9 @@
45144557
{
45154558
"cell_type": "code",
45164559
"execution_count": 89,
4517-
"metadata": {},
4560+
"metadata": {
4561+
"collapsed": true
4562+
},
45184563
"outputs": [],
45194564
"source": [
45204565
"# Rebuild KB because running fol_fc_ask would add new facts to the KB\n",
@@ -4951,7 +4996,7 @@
49514996
"name": "python",
49524997
"nbconvert_exporter": "python",
49534998
"pygments_lexer": "ipython3",
4954-
"version": "3.6.4"
4999+
"version": "3.6.1"
49555000
}
49565001
},
49575002
"nbformat": 4,

0 commit comments

Comments
 (0)