LOGIC VIA ASP
REASONING WITH
PROPOSITIONAL
LOGIC
Part of the M odule on Logic & Answer Set Pro log
M ichael Witb rock COM PSCI 367
2021 Semester 2 , Lecture 15
Some of these slides via
Dr. Patricia Riddle, chiefly from Dr Stuart Russell,
http://aima.cs.berkeley.edu/instructors.html, and some perhaps from other sources
Is Kyoto a City?
It’s a city if it’s the
capital of a country
It’s a city if it has more than 70000
inhabitants
Is Kyoto the
The capital of a country?
Nope (1869年以来)
X is number of inhabitants
of Kyoto
X > 70000
and
or
1.475 million is number of
inhabitants
of Kyoto
1.475 million >
70000
It’s a city
because
>70000
Yes
京都は
本当の都市
ですか？
Recall that our ultimate goal
is to solve problems by
automatically reasoning about
knowledge we already have
Knowledge level:
the point of computational logic
AI systems can be viewed at the knowledge level
i.e., what they know, regardless of how implemented
Or at the implementation level
i.e., data structures in KB and algorithms that manipulate them
8/24/2021 3COMPSCI 703 – Logic
• Trained deep learning systems can have knowledge and support inferences without involving logic
• Logic-based systems can acquire knowledge via learning
Propositional Logic is reliable,
but inexpressive
Mathematical
Logic
Computer
Programs
Careful Legal
Language
Scientific
Writing
Formal
Narrative
Informal
Narrative
Fiction
Poetry & Song
High precision and reliable reuse,
Low expressiveness
Low precision and usability
High expressiveness
natural language understanding
language understanding
formal languages
Review: Propositional logic: Syntax
Propositional logic is the simplest logic – illustrates basic ideas, and, in a sense, underlies ASP
The proposition symbols S1, S2 etc are sentences
If S is a sentence, S is a sentence (negation)
If S1 and S2 are sentences, S1 S2 is a sentence (conjunction)
If S1 and S2 are sentences, S1 S2 is a sentence (disjunction)
If S1 and S2 are sentences, S1 S2 is a sentence (implication)
If S1 and S2 are sentences, S1 S2 is a sentence (biconditional or equivalence)
8/24/2021 5
Review: Propositional logic: Semantics
Each model specifies true/false for each proposition symbol
E.g. P1,2 P2,2 P3,1
false true false
With these symbols, 8 possible models, can be enumerated automatically.
Rules for evaluating truth with respect to a model m:
S is true iff S is false
S1 S2 is true iff S1 is true and S2 is true
S1 S2 is true iff S1is true or S2 is true
S1 S2 is true iff S1 is false or S2 is true
i.e., is false iff S1 is true and S2 is false
S1 S2 is true iff S1S2 true and S2S1 true
Simple recursive process evaluates an arbitrary sentence, e.g.,
P1,2 (P2,2 P3,1) = true (true false) = true true = true
8/24/2021 6
Inference in the Wumpus world
An agent using propositional logic, just for pits, smell, breeze and wumpus:
P1,1
W1,1
Bx,y (Px,y+1 Px,y-1 Px+1,y Px-1,y)
Sx,y (Wx,y+1 Wx,y-1 Wx+1,y Wx-1,y)
W1,1 W1,2 … W4,4
W1,1 W1,2
W1,1 W1,3
…
64 distinct proposition symbols, 155 sentences1
8/24/2021 7CS367 – Logic
Note: the x,y here
must be instantiated to be
propositional formulas;
These are macros, not expressions
1 I haven’t checked the number of sentences, let me know if 155 is correct; you could write a small program for that
Wumpus KB contains “physics” sentences for every single square
For every time t and every location [x,y], you need a sentence like:
Ltx,y FacingRight
t Forwardt Lt+1x+1,y
Rapid proliferation of sentences!
BUT: this may not be a problem for a computer, depending on how the
proliferation happens
Expressivity limitation of propositional logic
8/24/2021 8CS367 – Logic
Review: Truth table for connectives
8/24/2021 9
• Propositional variables can only take two values, true and false
• Truth tables are easy to construct given the semantics of propositional logic (previous slide)
• The number of rows is exponential in the number of variables
Review: Truth tables for inference (does KB╞ α)
Enumerate rows (different assignments to symbols), if KB is true in row, check that α is too
8/24/2021 10
Our Wumpus KB
• No pit in [1,1]
• No Breeze in [1,1]
• Breeze in [2,1]
• A square is breezy if and
only if there is an adjacent
pit
P1,1 B1,1 B2,1
B1,1 (P1,2 P2,1)
B2,1(P1,1 P2,2 P3,1)
Our Query is α1
α1 = “[1,2] is safe“
S1,2
Review: What is a model?
◦A model of a KB (or equivalently of a theory) is an
assignment of values to all of its free variables which
makes all the sentences in that theory true.
◦ In the case of propositional logic, its an assignment of
True or False to each propositional variable (the things
between the connectives, like P or Q or P1,2) that makes
every sentence in the KB True
Validity
A sentence is valid if it is true in all models, e.g.:
◦ True
◦ A A
◦ A A
◦ (A (A B)) B
Validity is connected to inference via the Deduction Theorem:
KB ╞ α if and only if (KB α) is valid
i.e. a knowledge base entails a new theorem, if, and only if, in every model the
theorems in the KB cannot all be true without the new theorem being true
8/24/2021 12CS367 – Logic
Review: Satisfiability
A sentence is satisfiable if it is true in some model
e.g., A B, C, A B is satisfied by {A, B,C} (or A=False, B=True, C=True}
A theory (KB) is satisfiable if every sentence in the theory is true in some model
A sentence is unsatisfiable if it is true in no models
e.g., AA
Satisfiability is connected to one form of inference via the following:
KB ╞ α if and only if (KB α) is unsatisfiable
i.e., prove α by reductio ad absurdum (assume the opposite,
and show that it leads to an absurdity – i.e. something that can’t be true)
8/24/2021 13COMPSCI 367 – Logic
This will come up again when
we talk about answer sets
Proof methods
Proof methods divide into (roughly) two kinds:
Model checking: truth tables are one method
Application of inference rules: based on the idea of “logical equivalance”,
and the deduction theorem (a couple of slides back)
8/24/2021 14COMPSCI 703 – Logic
Logical equivalence
Two sentences are logically equivalent iff they are true in the same models: α ≡ ß iff α╞ β and β╞ α
8/24/2021 15COMPSCI 367 – Logic
Logical equivalences are the basis of inference rules
More than one name is
in use for each of these
equivalences: learn to
recognize them but not
necessarily to use these.
There are also inference
rules based on other
types of entailment than
logical equivalence
Application of inference rules
Legitimate (sound) generation of new sentences from old
Proof = a sequence of inference rule applications
Can use inference rules as operators in a standard search algorithm
Typically require transformation of sentences into a normal form
Forward & backward chaining
Resolution
8/24/2021 16
Model checking
◦ truth table enumeration (always exponential in n)
◦ improved backtracking
◦ Davis-Putnam-Logemann-Loveland (DPLL)
◦ heuristic search in model space
◦ sound but incomplete
◦ e.g., hill-climbing which minimises the number of unsatisfied clauses
8/24/2021 17
This is relevant to how answer
sets work, when we get to ASP
Forward and backward chaining
Horn Form (restricted) — KB = conjunction of Horn clauses
Horn clause =
proposition symbol; or
proposition symbol symbol; or
(conjunction of symbols) symbol
E.g., C; (B A); (C D B)
8/24/2021 18COMPSCI 703 – Logic
α1, … ,αn, α1 … αn β
β
Modus Ponens (for Horn Form): complete for Horn KBs
Can be used with forward chaining or backward chaining.
These algorithms are very intuitive and run in linear time
α: Socrates is a human
α β: Socrates is a human implies
that Socrates is mortal
β: Socrates is mortal
Forward vs. backward chaining
FC is data-driven, automatic, unconscious processing,
e.g., object recognition, routine decisions
May do lots of work that is irrelevant to the goal
BC is goal-driven, appropriate for problem-solving,
e.g., Where are my keys? How do I get into a PhD program?
Complexity of BC can be much less than linear in size of KB – because
we do not necessarily explore irrelevant nodes!!
8/24/2021 19CS367 – Logic
Forward chaining
Idea: fire any rule whose premises are satisfied in the KB,
add its conclusion to the KB, until query is found
8/24/2021 20COMPSCI 703 – Logic
Q is the
goal
Start with
the facts
Forward chaining example
8/24/2021 21CS367 – Logic
Forward chaining example
8/24/2021 22CS367 – Logic
Forward chaining example
8/24/2021 23CS367 – Logic
Forward chaining example
8/24/2021 24CS367 – Logic
Forward chaining example
8/24/2021 25CS367 – Logic
Forward chaining example
8/24/2021 26CS367 – Logic
Forward chaining example
8/24/2021 27CS367 – Logic
Forward chaining algorithm
Forward chaining is sound and complete for Horn KB
8/24/2021 28CS367 – Logic
Proof of
completeness
(not examinable)
FC derives every atomic sentence that is entailed by KB
1. FC reaches a fixed point where no new atomic
sentences are derived
2. Consider the final state as a model m, assigning
true/false to symbols
3. Every clause in the original KB is true in m
4. Proof: Suppose a clause a1 … akb is false in
m Then a1∧…∧ak is true in m and b is false in m
Therefore the algorithm has not reached a fixed point!
5. Hence m is a model of KB
6. If KB╞ q, q is true in every model of KB, including m
General idea: construct any model of KB by sound inference,
check α
8/24/2021 CS367 – Logic 29
Forward vs. backward chaining
FC is data-driven, automatic, unconscious processing,
e.g., object recognition, routine decisions
May do lots of work that is irrelevant to the goal
BC is goal-driven, appropriate for problem-solving,
e.g., Where are my keys? How do I get into a PhD program?
Complexity of BC can be much less than linear in size of KB – because
we do not necessarily explore irrelevant nodes!!
8/24/2021 30CS367 – Logic
Backward chaining
Idea: work backwards from the query Q:
to prove Q,
check if Q is known already, or
prove by backward chaining all premises of some rule concluding Q
Avoid loops: check if new subgoal is already on the goal stack
Avoid repeated work: check if new subgoal
1. has already been proved true, or
2. has already failed
Also avoids irrelevant work!!
31COMPSCI 703 – Logic
Q is the
goal
Start with
the qoal
Backward chaining example
8/24/2021 32CS367 – Logic
Backward chaining example
8/24/2021 33CS367 – Logic
Backward chaining example
8/24/2021 34CS367 – Logic
Backward chaining example
8/24/2021 35CS367 – Logic
Backward chaining example
8/24/2021 36CS367 – Logic
Backward chaining example
8/24/2021 37CS367 – Logic
Backward chaining example
8/24/2021 38CS367 – Logic
Backward chaining example
8/24/2021 39CS367 – Logic
Backward chaining example
8/24/2021 40CS367 – Logic
Backward chaining example
8/24/2021 41CS367 – Logic
Backward chaining example
8/24/2021 42CS367 – Logic
…
The Resolution inference rule
Modus Ponens (the method of putting) is not the only possible inference rule.
An alternative rule, resolution, works like this:
◦ Socrates is a not a person, or he is mortal, but
◦ Socrates is a person
◦ Therefore, Socrates is mortal
α1, … ,αn, α1 … αn β
β
In the forward and backward changing examples, we used Modus Ponens:
α β, α
β
Recall from logical equivalence:
Complementary Literals
In Wumpus World, resolution might look like this:
P1,3 P2,2, P2,2
P1,3
Resolution is sound and complete for complementary literals : it always works correctly,
and it is enough to prove everything that is entailed
8/24/2021 44CS367 – Logic
In the previous slide, the complementary literals {α , α} meant
{“Socrates isn’t a person”, “Socrates is a person”} respectively
Resolution
Conjunctive Normal Form (CNF): conjunction [“and”] of disjunctions [“or”] of literals
E.g., (A B) (B C D)
Resolution inference rule (for CNF): complete for propositional logic
l1 … li … lk, m1 …mj … mn
l1 … li … li-1 li+1 … lk m1 … mj-1 mj+1 … mn
where li and mj are complementary literals, i.e., li = mj, or, equivalently, mj = li,
8/24/2021 45CS367 – Logic
Strongly recommended: http://logic.stanford.edu/intrologic/notes/chapter_05.html
Why is Resolution sound?
Soundness of resolution inference rule:
(l1 … li-1 li+1 … lk) li
mj (m1 … mj-1 mj+1 … mn)
(l1 … li-1 li+1 … lk) (m1 … mj-1 mj+1 … mn)
This assumes li and mj are complimentary literals
(li and mj are equivalent, and so are li and mj)
(remember a b is equivalent to a b
since a b is equivalent to a b )
8/24/2021 46CS367 – Logic
Conversion to CNF: uses equivalences
B1,1 (P1,2 P2,1)
1. Eliminate , replacing α β with (α β)(β α).
(B1,1 (P1,2 P2,1)) ((P1,2 P2,1) B1,1)
2. Eliminate , replacing α β with α β.
(B1,1 P1,2 P2,1) ((P1,2 P2,1) B1,1)
3. Move inwards using de Morgan’s rules and double-negation:
(B1,1 P1,2 P2,1) ((P1,2 P2,1) B1,1)
4. Apply distributivity law ( over ) :
(B1,1 P1,2 P2,1) (P1,2 B1,1) (P2,1 B1,1)
8/24/2021 47CS367 – Logic
Resolution again in CNF
Soundness of resolution inference rule:
(l1 … li-1 li+1 … lk) li
mj (m1 … mj-1 mj+1 … mn)
(l1 … li-1 li+1 … lk) (m1 … mj-1 mj+1 … mn)
li and mj are complimentary literals
Notation: A sentence with just connectives is a clausal sentence.
E.g. l1 … lk, and {l1, …,lk} is the corresponding clause
8/24/2021 48CS367 – Logic
Resolution algorithm
8/24/2021 49CS367 – Logic
Proof by contradiction, i.e., show KBα unsatisfiable
The process continues until one of two things happens:
There are no new clauses that can be added, in which case KB does not entail α; or
Two clauses resolve to yield the empty clause, in which case KB entails α
Resolution Example
8/24/2021CS367 – Logic 50
KB = (B1,1 P1,2 P2,1)
(P1,2 B1,1)
(P2,1 B1,1)
B1,1
α = P1,2
(which still needs to be
negated!! As P1,2 or
P1,2
Pros and cons of propositional logic
☺ Propositional logic is declarative: pieces of syntax correspond to facts
☺ Propositional logic allows partial/disjunctive/negated information
◦ (unlike most data structures and databases)
☺Propositional logic is compositional:
◦ meaning of B1,1 P1,2 is derived from meaning of B1,1 and of P1,2
☺ Meaning in propositional logic is context-independent
◦ (unlike natural language, where meaning may depend on context)
☺ Propositional logic has methods for sound and complete inference
◦ (some logics don’t guarantee completness)
Propositional logic has very limited expressive power
◦ (unlike natural language)
◦ E.g., cannot say “pits cause breezes in adjacent squares“
◦ except by writing one sentence for each square
8/24/2021 51COMPSCI 703 – FOL
Summary
Logical agents apply inference to a knowledge base to derive new information and make decisions
Basic concepts of logic:
syntax: formal structure of sentences
semantics: truth of sentences wrt models
entailment: necessary truth of one sentence given another
inference: deriving sentences from other sentences
soundness: derivations produce only entailed sentences
completeness: derivations can produce all entailed sentences
Resolution is sound and complete for propositional logic
Forward, backward chaining are linear-time, complete for Horn clauses
Propositional logic lacks expressive power
8/24/2021 52CS367 – Logic
Remember:
WUMPUS KB contains “physics” sentences for every single square
For every time t and every location [x,y], Ltx,y FacingRight
t Forwardt Lt+1x+1,y
Rapid proliferation of clauses!!
Maybe there’s a way we could summarise all those facts
Expressiveness limitation of propositional
logic
8/24/2021 53COMPSCI 703 – Logic
Next,
FOL and then ASP
◦ We will generalise Propositional Logic to First
Order Logic, then
◦ We will simplify FOL a little,
◦ and change our epistemoligical
committment
◦ And use the result (ASP) to eventually (after
the break) build a simple grammatical parser
(becuase I like natural languages)
◦ Which ought to get you most of the way
towards solving the assignment , which you’ll
get on Sept 21st probably.
“Alice laughed. ‘There’s no
use trying,’ she said. ‘One
can’t believe impossible
things.’
I daresay you haven’t had
much practice,’ said the
Queen. ‘When I was your
age, I always did it for half-
an-hour a day. Why,
sometimes I’ve believed as
many as six impossible
things before breakfast.
There goes the shawl again
Through the Looking-Glass, and What Alice Found There (1871) Charles Lutwidge Dodgson
https://www.goodreads.com/author/show/8164.Lewis_Carroll