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:

KB = P(f(x)) -> P(x)
<=> ~P(f(x) v P(x)

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:

q :- p_1,p_2,...,p_n 

(i.e. "q, if p_1 and p_2 and ... and p_n)

This can be viewed as a procedure:

1. A goal literal matches (unifies) with q;
2. The tail of the clause "p_1 ... p_n" is instantiated with the substitution of values for variables (unifiers) derived from this match;
3. 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).

Outline

 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)

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.

Factorial

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))))

Fibonacci

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)))

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.

Other Examples

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).