Knowledge Representation II
FOL Resolution & Prolog
[AIMA 4G] Chapters 8 & 9
COSC1127/1125
Artificial Intelligence
Semester 2, 2021
Prof.
* The slides here are those from and KR book and ‘s one for Thinking as Computation book (see inside).
—
Wominjeka! Welcome!
I acknowledge, and invite you all to acknowledge, the Traditional Owners (Wurundjeri people of the Kulin Nations) of the land on which we will conduct this session for AI21. I recognise their continuing connection to land, waters and culture, as well as the challenges and injustices that continue up to our times, unfortunately.
IMPORTANT DISCLAIMER
These pack of slides are NOT core study
material. The core & main material is the book or any specific resources given for the week.
The slides in this presentations were prepared only for supporting the instructor during the lectorial and only some of them have been used in the session as needed.
These pack of slides do not represent the complete material of the week, but only a few bits here and there around what was discussed in lectorials. Most of the week content will NOT show up in this pack of slides.
Please refer to the book (and any resources specifically given) for a comprehensive coverage of the week material.
I have Pacman dreams…
Overview for …
Book-keeping info & news.
Questions?
From Propositional logic to FOL.
Objects, relations and functions
Logical equivalence.
FOL Resolution, unifiers, MGUs.
And more on inference….
Horn clauses, Prolog, forward/backward reasoning
‹#›
COSC1127/1125
AI’21 – Semester 2
Week 5 – KRR II
Prof.
WHAT IS THIS??
Some news…
Project 1 marks are coming this week
Was due 1 week ago only
Delayed for P2 team issues….
Project 2: Multi-agent Pacman
Group assignment.
No individual submissions without ELP or
PM exemption.
Remember silence policy from Friday COB
Project Contest:
From next week all the way to W12!
Same groups (with some changes, as needed)
*
Members contributions – Post #121
Remain professional:
Contribute.
Respect.
Acknowledge.
Appreciate.
Discuss openly.
Additional drop-in lab
Additional drop-in lab Wednesday
See post #117
If you book:
Make 100% you will use it.
Make a PRIVATE post before to inform us what you want to chat.
Include the link to your repo.
Remember Monday 4pm-5pm Consultation Time with Andres.
Book Consultation time with me on Tuesdays here
TODAY…
Beyond Propositional Logic.
First order logic for KR&R.
Talk about “objects” and quantify over them:
all x’s, some x’s
FOL reasoning:
FOL resolution
Prolog.
All this will be assessed in THE
Monday Sept 20th @ 9am – 9pm (12 hrs!).
No repeats or exceptions after it closes.
Make yourself available now for ~3hrs (if sharp).
Don’t take risks by leaving it too late.
Recommended to submit by 6pm at most.
Topics Week 1 – 8 (included).
Content from Book & Tutorials; no Pacman!
Answers entered ONLINE in a Google Form/Quiz:
Can use paper & pen for your notes.
Make sure you are logged into your RMIT Google Account (not your private account!)
You can submit once (as if handing in on paper)
No other submission allowed (e.g., email)
Will provide a “Sample” Exercise for dry-run.
No negative marking will be used! 🙂
Questions?
*
Recap: KR&R, Logic
Handling of knowledge is important & convenient for complex systems.
represent + reason about that knowledge.
knowledge-based systems.
Formal logic is one approach to KR&R:
Manipulation of symbols encoding propositions to produce representations of new propositions.
All about consequences.
What is true: KB |= α (α follows from KB)
all models of KB are models of α
Inference: syntactically deduce knowledge-level truth
from (¬A ∨ B) ∧ (¬B ∨ C) deduce (¬A ∨ C).
*
Logic, Proofs, Databases & AI
QUERY:
Is ɸ true?
ɸ1, ɸn, …, ɸn,
‹#›
L
O
G
I
C
Propositional Logic (recap)
Syntax – language:
Propositions: p, q, r, …
Connectives: ¬, ∧, ∨, →,↔,⊕
Boolean formulas
Semantics – meaning:
Truth assignment (to variables)
truth of boolean formulas derived
Truth-tables
Valid/tautology, contradiction, satisfaction
Equivalences
‹#›
(1848 – 1925)
mmm, how do I state that every human is mortal?
‹#›
Propositional vs first-order logic
Propositional logic:
propositions (p, q, r, etc.)
First-order logic:
Quantifiers, predicates, constants, variables, functions.
Syntactically different!
Are they equally expressive?
Prop logic → 1st-order logic: yes, all unary predicates
1st-order logic → prop logic: no, unless finite objects
Family Tree Domain in FOL
∀x Male(x) ⇔ ¬Female(x)
∀x, y Parent(x, y) ⇔ Child(y, x)
∀x, y Mother(x, y) ⇔ Female(x) ∧ Parent(x, y)
∀x, y Husband(x, y) ⇔ Male(x) ∧ Spouse(x, y)
∀x, y GrandParent(x, y) ⇔ ∃z Parent(x, z) ∧ Parent(z, y)
∀x, y Sibling(x, y) ⇔ ¬(x = y) ∧ ∃z Parent(z, x) ∧ Parent(z,y)
∀x, y Mother(motherOf(x), x)
[the mother of x (motherOf(x)) is the mother of x]
∀x,y primeMinister(x) = y ⇒ Citizen(y, x)
[if y is the prime minister of country x, then x is citizen of country x]
*
Quantifiers
“All men are mortal. Socrates is a man. So Socrates is mortal”
“Not all kangaroos are pink” vs “There is a non-pink kangaroo”
“Not always” vs “Sometimes not”
“Not any” vs “All not”
‹#›
How sharp is your logic?
Code 3721 2033 @ menti.com
‹#›
Quantifiers
“For every x there is a y such that P(x,y) is true”
“There is a y such that for every x P(x,y) is true”
P(x,y) is “y is the mother of x”
????
P(x,y) is “y is the mother of x”
‹#›
Family Trees
To make the kinship knowledge base complete some facts are needed, such as:
Parent(Mary, John)
Parent(George, John)
Spouse(George, Mary)
Male(George)
Female(Mary)
Parent (John, Henry)
Then we would answer queries like:
Who is the husband of Mary?
Is George Henry’s grandparent?
*
Entailment & Satisfiability
KB ╞ A
iff
interpretations that make KB true, make A true
(all models of KB are models of A )
iff
there is no model of KB ∧ ¬A
iff
KB ∧ ¬A is unsatisfiable
RESOLUTION
*
Programming in logic…
*
Family KB in Prolog (logic programming)
/* Facts */
male(jack).
male(simon).
male(harry).
female(helen).
female(sophie).
female(jess).
female(lily).
parent_of(jack,jess).
parent_of(jack,lily).
parent_of(helen, jess).
parent_of(helen, lily).
parent_of(oliver,james).
parent_of(sophie, james).
parent_of(jess, simon).
parent_of(ali, simon).
parent_of(lily, harry).
parent_of(james, harry).
/* Rules */
father_of(X,Y):- male(X),
parent_of(X,Y).
mother_of(X,Y):- female(X),
parent_of(X,Y).
grandfather_of(X,Y):- male(X),
parent_of(X,Z),
parent_of(Z,Y).
grandmother_of(X,Y):- female(X),
parent_of(X,Z),
parent_of(Z,Y).
sister_of(X,Y):- %(X,Y or Y,X)%
female(X),
father_of(F, Y), father_of(F,X),X \= Y.
The House Puzzle
Five colored houses in a row, each with an owner, a pet, cigarettes, and a drink.
The English lives in the red house.
The Spanish has a dog.
They drink coffee in the green house.
The Ukrainian drinks tea.
The green house is next to the white house.
The Winston smoker has a serpent.
In the yellow house they smoke Kool.
In the middle house they drink milk.
The Norwegian lives in the first house from the left.
The Chesterfield smoker lives near the man with the fox.
In the house near the house with the horse they smoke Kool.
The Lucky Strike smoker drinks juice.
The Japanese smokes Kent.
The Norwegian lives near the blue house.
Who owns the zebra and who drinks water?
SWI Prolog
The House Puzzle in Logic!
Logic Programming in action @ ICAPS’21
More reading on other sources…
FOL Resolution & Horn clauses Sections 4 & 5
Prolog
Sections 3, 4 & 7
*
Pointers to MGU & FOL resolution
Skolemization, Most General Unifiers, First-Order Resolution
Finding the most general unifier
Interesting post in stackoverflow: Is the following a unifier, but not a most general unifier?
Conclusion
FOL used for KR&R.
Beyond propositional logic.
Reason about “objects”
Adds constants, variables, functions,
predicates & quantification (∀, ∃).
FOL resolution:
substitution, unifier, MGU.
skolemization for functions.
Logic Programming/Prolog:
SLD-resolution
for Horn clauses
(at most 1 positive literal per clause)
*
Whiteboards used during lectorials