人工智慧/符號程式設計
KB = P(f(x)) -> P(x) <=> ~P(f(x) v P(x)
假設我們要證明 P(a)。歸結反駁假設否定目標 - ~P(a) 並從 ~P(f(x)) v P(x) 中，我們可以透過將 "a" 替換為 "x" 來推匯出 P(f(a))。然後，我們可以繼續再次歸結以獲得 P(f(f(a))) 等等。這是否與歸結反駁是完整的斷言相矛盾？不，因為完整性指出任何可以透過歸結從一組前提 P 推匯出的句子 Q 必須由 P 推出。如果它不是由 P 推出的，那麼我們可能無法證明它！
命題邏輯是可判定的。
霍恩子句 = 最多隻有一個肯定文字的子句（在 Prolog 中："q :- p_1, p_2, ... , p_n" 代表霍恩子句 "q v ~p_1 v ~p_2 v ... v ~p_n"）。
Prolog 語法基於霍恩子句，其形式為 "p_1,p_2,...,p_n -> q"。在 Prolog 中，這對映到一個 "if-then" 子句
q :- p_1,p_2,...,p_n
（即 "q, if p_1 and p_2 and ... and p_n"）
這可以被視為一個過程
- 一個目標文字與 q 匹配（統一）；
- 子句的尾部 "p_1 ... p_n" 用從這種匹配中得出的變數的值（統一器）的替換來例項化；
- 例項化的子句作為呼叫其他過程的子目標，依此類推。
Prolog 的定理證明方法是歸結反駁（假設否定假設並嘗試歸結空子句）- 如果你成功了，那麼可以安全地斷言假設，否則不能。歸結僅適用於矛盾文字（例如，{~p,q},{p} 代表 "如果蘇格拉底是人（p），那麼他是凡人（q）" 在 CNF 中（p 意味著 q 等同於 ~p 或 q）；現在，如果我們假設蘇格拉底確實是人，那麼透過歸結，這將意味著 q）。
如果我們有一個目標 q，那麼斷言否定目標進行歸結反駁可能是有意義的，這本質上是歸謬證明。這是一種帶有子目標的反向推理形式：我們斷言否定目標並嘗試反向工作，統一和歸結子句，直到我們得到空子句，這使我們能夠聲稱該理論意味著我們最初的假設（透過歸謬）。
Input = Query Q and a Logic Program P;
Output = "yes" if Q follows from P, "no" otherwise;
Initialize current goal set to {Q}
While(the current goal set is not empty) do
Choose a G from the current goal set (first)
Look for a suitable rule in the knowledge-base;
unify any variable if necessary to match rule;
G :- B1, B2, B3, ...
If (no such rule exists) EXIT
Else Replace G with B1, B2, B3...
If (current goal set is empty)
return NO.
Else
return YES. (plus all unifications of variables)
Prolog 中的剪枝 (!) 不健全！
Prolog 本身（即使不考慮 "否定失敗" (\+) 和剪枝也不完整。
Prolog 使用線性輸入歸結（歸結公理和目標，然後是公理和新歸結的子目標，等等，並且 *從不* 歸結兩個公理）。
CDR 生成列表的剩餘部分，CAR 生成列表的頭部。Lisp 程式是包含 S 表示式的 S 表示式。因此，基本上，Lisp 程式是處理連結列表的連結列表。
Prolog:
factorial(1,1).
factorial(N,Result) :- NewN is N-1,
factorial(NewN,NewResult),
Result is N * NewResult.
Tail recursion:
factorial(N,Result) :- fact_iter(N,Result,1,1).
fact_iter(N,Result,N,Result) :- !.
fact_iter(N,Result,I,Temp) :- I < N,
NewI is I+1,
NewTemp is Temp * NewI,
fact_iter(N,Result,NewI,NewTemp).
Lisp:
(defun factorial (n)
(cond
((<= n 1) 1)
(* n (factorial (- n 1)))))
Tail recursion:
(defun fact_tail (n)
(fact_iter 1 1 n))
(defun fact_iter (result counter max)
(cond
((> counter max) result)
(T (fact_iter (* result counter) (+1 counter) max))))
Prolog:
fib(1,1). fib(2,1).
fib(N,Result) :- N > 2,
N1 is N-1,
N2 is N-2,
fib(N1,F1),
fib(N2,F2),
Result is F1 + F2.
Tail recursion:
fibo(N,Result) :- fib_iter(N,Result,1,0,1).
fib_iter(N,Result,N,_,Result) :- !.
fib_iter(N,Result,I,F1,F2) :- I < N,
NewI is I+1,
NewF1 is F2,
NewF2 is F1+F2,
fib_iter(N,Result,NewI,NewF1,NewF2).
Lisp:
(defun fib (n)
(cond
((<= n 2) 1)
(+ (fib (- n 1)) (fib (- n 2)))))
Tail recursion:
(defun fib-tail (n)
(fib_iter 1 1 0 1 n))
(defun fib-iter (result counter f1 f2 max)
(cond
((> counter max) result)
(T (fib-iter (+ f1 f2)
(+1 counter)
f2
(+ f1 f2)
max)))
程式從程式內部遞迴呼叫自身。使用堆疊儲存等待來自較低級別的結果的中間狀態。遞迴下降到停止條件，該條件返回一個確定性的結果，該結果傳遞到下一個較高級別，直到我們再次到達頂層。最終結果是在途中計算出來的。
在尾遞迴中，遞迴呼叫是程式中的最後一個呼叫。這使我們能夠在遞迴下降時構建結果，直到我們到達底層；在此過程中，我們計算最終結果，以便一旦我們到達停止條件，該結果就可用。“智慧”編譯器識別尾遞歸併在我們到達底部時停止程式 - 但一些編譯器會在返回結果之前將結果“冒泡”到頂層。
Flatten
(defun flatten (thelist)
(if
((null thelist) nil)
((atom thelist) (list thelist))
(t (append (flatten (car thelist)))
(flatten (cdr thelist)))))
REVERSE
(defun myrev (thelist)
(if
((null thelist) nil)
(append (myrev (cdr thelist)) (list (car thelist))
DELETE ELEMENT (Prolog)
del(X,[X|Tail],Tail).
del(X,[Y|Tail],[Y|Tail1]) :- del(X,Tail,Tail1).
FLATTEN (Prolog)
flat([],[]). flat([Head|Tail],Result) :- is_list(Head),
flat(Head,FlatHead),
flat(Tail,FlatTail),
append(FlatHead,FlatTail,Result).
flat([Head|Tail],[Head|FlatTail]) :- \+(is_list(Head)),
flat(Tail,FlatTail).
Union set
union([],Set,Set).
union([Head|Tail],Set,Union) :- member(Head,Set),
union(Tail,Set,Union).
union([Head|Tail],Set,[Head|Union]) :- \+(member(Head,Set)),
union(Tail,Set,Union).