AI Mini Project
Group Members:
Sr. No. Name Roll Number
1 Gavin Pereira 47
2 Shruti Shelar 61
3 Aveesah Siddiqui 63
Story:
(a) Emily was a woman.
(b) Emily was a scientist.
(c) All women are individuals.
(d) Einstein was a physicist.
(e) All scientists either admired Einstein or disagreed with him (or both).
(f) Everyone admires someone.
(g) Individuals only criticize physicists they do not admire.
(h) Emily criticized Einstein.
To prove: Emily disagreed with Einstein.
Proof:
Step 1: Represent the statements in first-order logic:
(a) Emily was a woman
woman(Emily)
(b) Emily was a scientist.
scientist(Emily)
(c) All women are individuals.
∀x woman(x) → individuals(x)
(d) Einstein was a physicist.
physicist(Einstein)
(e) All scientists either admired Einstein or disagreed with him (or both).
∀x scientist(x) → (admired(x, Einstein) ∨ disagreed(x, Einstein))
(f) Everyone admires someone.
∀x∃y admired(x, y)
(g) Individuals only criticize physicists they do not admire.
∀x∀y individual(x) ∧ physicists (y) ∧ criticize(x, y) → ¬ admired(x, y)
(h) Emily criticized Einstein.
criticize(Emily, Einstein)
Step 2: Negate the statement to be proved:
¬ disagreed(Emily, Einstein)
Step 3: Convert the first-order-logic to conjunctive normal form:
Step 3.1: Remove Implications
(a) Emily was a woman
woman(Emily)
(b) Emily was a scientist.
scientist(Emily)
(c) All women are individuals.
∀x ¬ woman(x) ∨ individuals(x)
(d) Einstein was a physicist.
physicist(Einstein)
(e) All scientists either admired Einstein or disagreed with him (or both).
∀x ¬ scientist(x) ∨ (admired(x, Einstein) ∨ disagreed(x, Einstein))
(f) Everyone admires someone.
∀x∃y admired(x, y)
(g) Individuals only criticize physicists they do not admire.
∀x∀y ¬ (individual(x) ∧ physicists(y) ∧ criticize(x, y)) ∨ ¬ admired(x, y)
(h) Emily criticized Einstein.
criticize(Emily, Einstein)
Step 3.2: Move negation inwards and rewrite:
(a) Emily was a woman
woman(Emily)
(b) Emily was a scientist.
scientist(Emily)
(c) All women are individuals.
∀x ¬ woman(x) ∨ individuals(x)
(d) Einstein was a physicist.
physicist(Einstein)
(e) All scientists either admired Einstein or disagreed with him (or both).
∀x ¬ scientist(x) ∨ (admired(x, Einstein) ∨ disagreed(x, Einstein))
(f) Everyone admires someone.
∀x∃y admired(x, y)
(g) Individuals only criticize physicists they do not admire.
∀x∀y ¬individual(x) ∨ ¬ physicists(y) ∨ ¬ criticize(x, y) ∨ ¬ admired(x, y)
(h) Emily criticized Einstein.
criticize(Emily, Einstein)
Step 3.3: Skolemization (replace existential quantifiers with Skolem functions):
(a) Emily was a woman
woman(Emily)
(b) Emily was a scientist.
scientist(Emily)
(c) All women are individuals.
∀x ¬ woman(x) ∨ individuals(x)
(d) Einstein was a physicist.
physicist(Einstein)
(e) All scientists either admired Einstein or disagreed with him (or both).
∀x ¬ scientist(x) ∨ (admired(x, Einstein) ∨ disagreed(x, Einstein))
(f) Everyone admires someone.
∀x admired(x, f(x))
(g) Individuals only criticize physicists they do not admire.
∀x∀y ¬individual(x) ∨ ¬ physicists (y) ∨ ¬ criticize(x, y) ∨ ¬ admired(x, y)
(h) Emily criticized Einstein.
criticize(Emily, Einstein)
Step 3.4: Rename Variables:
(a) Emily was a woman
woman(Emily)
(b) Emily was a scientist.
scientist(Emily)
(c) All women are individuals.
∀x ¬ woman(x) ∨ individuals(x)
(d) Einstein was a physicist.
physicist(Einstein)
(e) All scientists either admired Einstein or disagreed with him (or both).
∀y ¬ scientist(y) ∨ (admired(y, Einstein) ∨ disagreed(y, Einstein))
(f) Everyone admires someone.
∀z admired(z, f(z))
(g) Individuals only criticize physicists they do not admire.
∀a∀b ¬individual(a) ∨ ¬physicists(b) ∨ ¬ criticize(a, b) ∨ ¬ admired(a, b)
(h) Emily criticized Einstein.
criticize(Emily, Einstein)
Step 3.5: Drop Universal Quantifiers:
(a) Emily was a woman
woman(Emily)
(b) Emily was a scientist.
scientist(Emily)
(c) All women are individuals.
¬ woman(x) ∨ individuals(x)
(d) Einstein was a physicist.
physicist(Einstein)
(e) All scientists either admired Einstein or disagreed with him (or both).
¬ scientist(y) ∨ admired(y, Einstein) ∨ disagreed(y, Einstein)
(f) Everyone respects someone.
admired(z, f(z))
(g) Individuals only criticize physicists they do not admire.
¬ individual(a) ∨ ¬ physicists (b) ∨ ¬ criticize(a, b) ∨ ¬ admired(a, b)
(h) Emily criticized Einstein.
criticize(Emily, Einstein)
Step 4: Resolution:
(e) disagreed(y, Einstein)
¬ disagreed(Emily, Einstein)
{Emily/y}
¬ scientist(Emily) ∨ (b) scientist(Emily)
admired(Emily, Einstein)
(g) ¬ admired(a, b)
admired(Emily, Einstein)
{Emily/a , Einstein/b}
¬ individual(Emily) ∨ (c) individuals(x)
¬physicists(Einstein) ∨
{Emily/x}
¬criticize(Emily, Einstein)
¬ woman(Emily) ∨ (a) woman (Emily)
¬physicists(Einstein) ∨
¬criticize(Emily, Einstein)
¬physicists(Einstein) ∨ (d) physicists(Einstein)
¬criticize(Emily, Einstein)
(h) criticize(Emily, Einstein)
¬criticize(Emily, Einstein)
Now, we have derived ¬criticize(Emily, Einstein)). This contradicts clause (h), which states
criticize(Emily, Einstein). Since Emily criticized Einstein, this leads to a contradiction.
Therefore, our original assumption that Emily did not disagree with Einstein (¬disagreed(Emily,
Einstein)) must be false.
Thus, we can conclude that Emily did indeed disagree with Einstein: disagreed(Emily, Einstein).
