訊息
|
布林邏輯、謂詞邏輯與一階邏輯是最常被使用的兩種邏輯系統，布林邏輯在電路設計上有強大的用途，而一階邏輯則成為人工智慧領域的理論基礎。
謂詞邏輯乃是布林邏輯的延伸，此種邏輯具有一種類似布林函數的基本元素，通常稱為謂詞 (Predicate)，因此稱為謂詞邏輯 (Predicate Logic) 。
一階邏輯乃是謂詞邏輯的延伸，包含兩個很特別的量詞運算，全部 (forall) 與存在 (exist) 等，如果我們不處理這兩個運算，則將退化為謂詞邏輯。
由於引入謂詞之後，就必然要面對到底是全部還是部分的問題，因此通常我們所稱的謂詞邏輯就是一階邏輯。
人工智慧版
Chapter 7: First order logic
Constant + Predicate + Function = First Order Logic
Term : Constant , variable or Function
Ground Term : A term with no variable
Atomic Sentence : Predicate with parameter.
Complex Sentence : Sentence with logical connective.
Quantifier : $, #, #!,
Second Order Logic : $p φ
Situation calculus :
1. Special time sequence variable called situation :
S0,S1,S2,.. , St, …
2. Result(action, Si)=Si+1
3. Effect axiom : axioms that make the world change.
Ex: -Hold(x, Result(Release, s))
4. Frame axioms : axioms that describe how the world stay the same.
Ex: -Hold(x,s)^(a≠Grab├(Present(x,s)^Portable(x))=>-Hold(x,Result(a,s))
5. Successor-state axiom = Effect axiom + Frame axiom
Ex: Hold(x,Result(a,s))
<=>[(a=Grab^Present(x,s)^Portable(x))|(Hold(x,s)^a≠Release)]
Representational Frame Problem :
The proliferation of frame axioms (solved by Successor-state axiom)
Inferential Frame Problem :
When reasoning about the result or a long sequence of action in situation calculus, we have to carry each property through all intervening situation one step at a time, even if the property remain unchanged throughout.(this is why that special purpose reasoning system such as planning system is needed).
Qualification :
it’s difficult to define the circumstances under which a given action is guaranteed to work.
Ramification Problem :
it’s almost impossible to describe all the implicit consequence of actions.
Deduce Hidden Properties of the World
Synchronic rules :
relate properties of a world property of the world causes certain percepts to be generated.
(Type1) Causal rules : Conclusion => Environment
(Type2) Diagnostic rules : Percept => Conclusion
計算理論版
Chapter 5: First Order Logic
Syntax :
Vocabulary : Σ = (Φ, π, r)
Φ : a set of function symbol
π : a set of relation symbol
r : Φ ∪ π --> N , arity function
Remark1 :
if f in Φ and r(f) = 0 then f is called a constant
Remark2:
We can treat Boolean logic as a special case of first order logic, in which Φ = empty and r(p) = 0 for all p in π
Remark3:
The text book require the arity of a relation symbol cannot be 0, in which case lemma 2 does not apply.
V = {x, y, z, ... } , a countably infinite set of variable
T(Φ, V) : set of terms
(1) V in T(Φ, V)
(2) if f in Φ , r(f) = k and t1... tk in T(Φ, V)
then f(t1...tk) in T(Φ, V)
A(Φ, π, V) : set of atomic expression
if p in π, r(p) = k, t1...tk in T(Φ, V)
then p(t1...tk) in A(Φ, π, V)
F(Φ, π, V) : set of first order expression(first order formulas)
(1) A(Φ, π, V) in F(Φ, π, V)
(2) if φ, ψin F(Φ, π, V)
then -φ, φ|ψ, φ ψin F(Φ, π, V)
(3) if φ in F(Φ, π, V) and x in V
then x φ, x φin F(Φ, π, V)
f(x)|g(x) is wrong
P(f(x))|Q(g(x)) is correct.
Model Theory of First Order Logic :
Given Σ a model appropriate to Σ is a pair of M = (U, μ)
where U ≠ Empty
U : universe of M
μ: V-> U , for every variable we assign an interpretation X(μ)
for every function f in Φ of arity k , μ assign a function f(μ): Uk->U
for every predicate P in π of arity k, μ assign a set of k tuple Pk in Uk
Given formula Φin F(Φ, π, V) μ satisfied Φ iff
(1) Φ is an atom P(t1,…,tn) and <t1M…tnM> in PM
Example : M satisfied P(a,x) if aM=0 , xM=3, PM = {<x,y>; x < y}
(2) Φ IS -P and M satisfied P
(3) Φ is P&Q and M satisfied P and M|=Q
Φ is P|Q and M satisfied P or M|=Q
Φ is P=>Q and M not satisfied P and M|=Q
(4) Φ is X P and for every u in U μ(x=u) |= P
Φ is X P and there is a u in U s.t. μ(x=u) |= P
Given M, u in U definedμM(x=u)=u
Proposition : let P be an expression, and M as M' be two model s.t. they differ only on variables in P, then M|=P iff M'|=P
Remark : when consider the satisfiability or validity of sentence we do not need to worry about how the variable are interpreted in the model.
A sentence is valid if it is true in all models.
A sentence is unsatisfiable if it is not true in any model.
Theorem : there is a model N' s.t. for all sentence P expressible in the language of number theory , N|=P iff N'|=P
Remark : Axiomitization (N cannot be axiomitization by the language of N, but G, N mod p can )
Proof Theory :
Axiom 0 : tautulogies
Axiom 1 : 1. t=t
2. t1 = t1' & t2=t2' &…&tn=tn' f(t1,..,tn) = f(t1',..,tn')
3. t1 = t1' & t2=t2' &…&tn=tn' & R(t1,…,tn) R(t1',.., tn')
Axiom 2 : x PP[x=t] when t is a term
Axiom 3 :P x P x is not free in P
Axiom 4 : x (PQ) (x P xQ)
Modus Ponens P; PQ Q
example :
P(f(a), x)|Q(f(y), g(a, y)) --> ψ
P(f(a), x)|Q(f(y), g(a, y)) --> F
Example : number theory
Φ = {0, succ, +, *, ^ }
π = { < } // recall that = is always exist
Note 1 : we can use 1 as a shorthand for succ(0)
Example : graph theory
Φ = Empty
π = {G} r(G) = 2
Undirected Graph
xy G(x,y) G(y,x)
Transitivity
xyG(x,y) & G(y,z) G(x,z)
A variable is free if it is not within the scope of any x or x
Otherwise, x is bound
A sentence is a FOE without any free variable.
Theorem :
For any expression φ over Σ(G), the problem φ-graph is in P
Semantic :
Proposition
1 : if φ is unsatisfiable (has no model) then ╞ -φ
An expression is unsatisfiable iff its negation is valid.
2 : Boolean Validity :
Suppose that Boolean form of an expression φ is a tautology, then φ is valid.
3 : Equality :
(t1=t1' & ... & tk = tk') => f(t1,...,tk)=f(t1',...,tk')
(t1=t1' & ... & tk = tk') => R(t1,...,tk)=R(t1',...,tk')
4 : Quantifiers :
4.1 Any expression of the form φ => φ[x<-t] is valid.
4.2 If φ is valid, then so is xφ
4.3 If x does not appear free in φ, then φ => x φ is valid.
4.4 For all φ and ψ, (x (φ=>ψ)) => ((x φ)=> (x ψ))
Hilbert Style Proof Theory
1. Axioms :
AX0: Any expression whose boolean form is a tautology.
example :
x P(x) => x P(x) , its boolean form (A=>A) is a tatulogy.
x P(x) => P(X), has no exact boolean form.
AX1:
AX1a: t = t for every t in T(F, x)
AX1b: t1=t1'&t2=t2'&..&tn=tn' => f(t1,...,tn)=f(t1',...,tn')
AX1c: t1=t1'&t2=t2'&..&tn=tn'&R(t1,...,tn)=> R(t1',...,tn')
AX2: Any expression of the form x φ=>φ[x<-t]
AX3: Any expression of the form φ=>x φ, with x not free in φ
AX4: Any expression of the form (x (φ=>ψ))=>( xφ=> xψ)
illogical 不合邏輯的
alogical 非關邏輯的
Derivation (├)
given a set of expression Δ and an expression φ, Δ├φ (Δ derive φ or φ is a theorem of Δ) if there is a finite sequence of expression (φ1,..., φn) s.t :
(1) φn = φ
(2) For all 1≦i≦n φI in Λ ∪ Δ or j,k<i s.t φj is φk=>φi
If ├φ then φ is a theorem
Theoremhood : Given φ , is ├φ
Theorem : Theoremhood is recursive enumerable
Deductive Theorem
If Δ ∪ {φ} ├ ψ then Δ ├ φ=>ψ
Proof:
(Induction in the length of sequence of derivation)
Consider a proof of S=(φ1,...,φn) of ψ from Δ ∪ {φ}
(ie : φn = ψ)
Suppose that for all j<i, φ=>φj
if φi in Δ ∪ Λ then
φi (by hypothesis), φi=>(φ=>φi) (by axiom) so φ=>φi
else // if φi not in Δ ∪ Λ then
the proof include φ=>φj, φ=>(φj=>φi)
(by induction hypothesis)
and (φ=>φj)=>((φ=>(φj=>φi))=>(φ=>φi)) is a tautology
so (φ=>(φj=>φi))=>(φ=>φi) by MP
φ=>φi by MP
so by induction, Δ ├{φ}=>φn(= ψ)
Facebook
|
Post preview:
Close preview