人工智能/符号编程
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).