# Artificial Intelligence/Symbolic Programming
## Algorithms in PROLOG

* Subset of First Order Logic
* restricted to Horn Clauses
* Inference by resolution theorem proving
* Unification
* Depth-First-Search
* Backward-Chaining Approach

### Inner workings

Resolution is semi-decidable for First Order Logic:
and let's say we're trying to prove P(a). Resolution refutation assumes the negated goal - ~P(a) and from ~P(f(x)) v P(x) we can derive P(f(a)) by substituting "a" for "x". But then we can go on and resolve again to get P(f(f(a))) etc. Does this contradict the claim that resolution refutation is complete? NO - because completeness states that any sentence Q that can be derived by resolution from a set of premises P must be entailed by P. If it is not entailed by P, then we might no be able to proof that!
Propositional calculus is decidable.
Horn Clause = clause with at most one positive literal (in Prolog: "q :- p_1, p_2, ... , p_n" stands for the Horn Clause "q v ~p_1 v ~p_2 v ... v ~p_n".
Prolog syntax is based on Horn clauses, which have the form of "p_1,p_2,...,p_n -> q". In Prolog, this is mapped to an "if-then"-clause:
(i.e. "q, if p_1 and p_2 and ... and p_n)
This can be viewed as a procedure:
* A goal literal matches (unifies) with q;
* The tail of the clause "p_1 ... p_n" is instantiated with the substitution of values for variables (unifiers) derived from this match;
* The instantiated clauses serve as subgoals that invoke other procedures and so on.
Theorem-proving method of Prolog is resolution refutation (assume the negated hypothesis and try to resolve the empty clause) - if you succeed, then it's safe to assert the hypothesis, otherwise not. Resolution simply works on contradictory literals (e.g. {~p,q},{p} stands for "if socrates is a man (p) then he is mortal (q)" in CNF (p implies q is equivalent to ~p or q); now if we assume that socrates is indeed a man, then by resolution, this implies q).
If we have a goal q, then it might make sense to assert the negated goal for resolution refutation, which is essentially proof by reductio. This is a form of backward reasoning with sub-goaling: we assert the negated goal and try to work backwards, unifying and resolving clauses until we get to the empty clause, which allows us to claim that the theory implies our original hypothesis (by reductio).

### Cuts

Cuts (!) in Prolog are NOT sound!
Prolog itself (even if not considering the "failure by negation" (\+) and the cut is NOT complete.
Prolog uses Linear Input Resolution (resolve axiom and goal, then axiom and newly resolved subgoal, etc. and never resolve two axioms).

## Algorithms in LISP

CDR yields rest of the list, CAR yields head of the list. Lisp programs are S-expressions containing S-expressions. So basically, a LISP program is a linked list processing linked lists.

## Recursion
### Standard Recursion

Program calls itself recursively from within the program. Uses a stack to store intermediate states that "wait" for a result from a lower level. The recursion goes down to a stopping condition, which returns a definite result that is passed on to the next higher level until we reach the top level again. The final result is computed along the way.

### Tail Recursion

In tail recursion, the recursive call is the last call in the program. This allows us to build up the result while we're going down in the recursion until we hit the bottom level; along the way, we compute the final result, such that it is available once we reach the stopping condition. "Smart" compilers recognize tail recursion and stop the program once we hit the bottom - but some compilers "bubble" the result up to the top level before returning it.