In arithmetic we have infinitely many facts that increase natural numbers
by 1. For example
1+1=2
1+2=3
...
1+n=n+1
...
In logic we can satisfy all the above with a single term:
forall n: (1+n=n+1)
But what about other rules of arithmetic? We will end up with an infinite number of these rules.
Knowledge Base is a finite set of formulas of some logical systems.
Operations: logical inference, ...
KB is a subset of Implicit knowledge, a set of all formulas that can be deducted from KB using the inference engine of the logic used.
In the example of 1+n above 1+7=7+1 is in this set. Based on the KB we
know this is true provided that the AI agent "knows" arithmetic.
Definition A logic is a pair: < L, |-- > where L is the language and |-- is the inference operation.
X |-- A (where X is a set of formulas and A is a formula) is read "X infers A" or "A can be deducted from X".
Definition: A relation |-- is said to be an (A.Tarski) inference operation if:
Proof: If X |-- A, then A E C(X) so by (1): C(X) |-- A C(X) C C(C(X)) -- follows from 1 and 2 C(C(X)) C C(X) if A E C(C(X)), then A E C(X) if C(X) |-- A, then X |-- A
PC = < LPC, |--PC >
Definition: The set FOR of formulas of PC is the smallest set such that:
¬a, avb, a^b, a->b,
a = b
are in FOR p1, q1, r in FOR (by 1) p1q1p1 not_in FOR p1vq1, ¬r in FOR (by 2) (AA) (p1vq1)-> ¬r in FOR (by 2 and AA above)
E.g. converting
(p1^q1)v...v(p100^q100) to
CNF and preserving logical
equivalence:
α in CNF of O(2100) symbols
A literal is a variable or the negation of a variable.
A clause is a disjunction of 1 or more literals. e.g. ¬p v ¬p, ¬p and ¬p v p v q are clauses
Note: The empty clause (∅) means "inconsistency".
CNF-formula: A formula is in conjunctive normal form if it is a conjunction of 1 or more clauses. e.g. (p)^(¬q v s v t)^(¬s v ¬t)
Fact: For every formula alpha of PC there exists a CNF-formula αCNF such that α = αCNF
Notation for CNF-formulas:
a ^ b = b ^ a a ^ b = 1 iff a = 1 and b = 1 Instead of c1^c2^...^cn for a CNF-formula, we should write {c1,c2,...,cn}
We want to represent knowledge as a set up clauses: (S is the clausal representation)
We need to go from PC = < L, |--CP > to PCC = < LC, |--CP > (The predicate logic of clauses)
AI agent knows what α means (KB |-- α).
Semantics: we have 2 truth values:
The meaning of symbols:
Example: Let α = p --> (q v ¬s) = ¬p v (q v ¬s) = ¬p v q v ¬s h(p) = 1 h(q) = 0 h(s) = 0 h(α) = max(h(¬p), h(q), h(¬s)) = max(1 - h(p), h(q), 1 - h(s)) = max(0,0,1) = 1
Definition: Formula α is satisfiable iff there exists a truth-value assignment h such that h(α) = 1.
Definition: A formula α is a tautology iff for every truth-value assignment h, h(α) = 1. (e.g. p --> p)
Definition: A formula α is said to be contradictory iff ¬α is a tautology, or, equivalently, for every truth-value assignment h, h(α) = 0. (e.g. ¬(p --> p))
Definition: A set X of formulas is consistent iff there exists a
truth-value assignment h, such that h(X) = {1}.
(Note: if X = {α1, ..., αc, } then
h(X) = {h(α1), ..., h(αc)})
e.g. we have EX = {p v q, ¬p v q, p v ¬q} and
h(p) = h(q) = 1 thus h(EX) = {1}
Definition: A set X is inconsistent iff it is not consistent.
EX1 = {p v q, ¬p v q, p v ¬q, ¬p v ¬q} Suppose EX1 is consistent, So there is h s.t. h(EX1) = {1} CASE1: h(p) = 0. In this case EX1 reduces to: {q, 1, ¬q, 1} | | Contradiction CASE2: h(p) = 1 from EX1 we get: {1, q, 1, ¬q} | | Contradiction Conclusion: There is no assignment h s.t. h(EX1) = {1}
Objective: To define the inference operation: X |--PC α
(X |--PC α) iff for every truth-value assignment h, if h(X) = {1}, then h(α) = 1. (Note: ø |-- α is true)
The only difference between PC = < L, |--CP > and PCC = < LC, |--CP > is that the later is a language of clauses.
Example:
Is {p, p --> q} |--PC q true?
Suppose it is not true, then by the definition of |--PC there is h
such that:
(a) h(p) = h(p --> q) = 1
(b) h(q) = 0
By the definition, h(p --> q) = h(¬p v q)
= max(h(¬p), h(q)) = max(1 - h(p), h(q))
[by (a)] = max(0, h(q)) = 1
But h(q) must be 1, contradicting (b)
Thus, {p, p --> q} |--PC q is true
Another example:
ø |--PC p --> (p v q) ?
By the definition of |--PC, we need:
- for every h, if h(ø) C {1} then h(p --> (p v q)) = 1
- for every h, if true, then h(p --> (p v q)) = 1
-- But 1 --> β = β (for any variable β)
--> for every h, h(p --> (p v q)) = 1 ((p v q) is always true)
The first algorithm to implemenet |--PC
INPUT: A finite set X of formulas, a formula α
OUTPUT: YES iff X |--PC α
METHOD:
Let p1, ..., pn be all the propositional variables
that occur in formulas of X and in α
Let h1, ..., h2^n, i = 1
STEP1: if hi(X) C {1} but hiα = 0
then return NO
STEP2: if i = 2^n then return YES
else {i = i+1;
go to STEP 1}