Translating to Predicate Logic 
==============================


A HORN CLAUSE is a disjunction of literals (where a literal is a negated or unnegated predicate)
under the  restriction to contain at most one unnegated literal i.e. positive literal.

ex :

~A V ~B V ~C V H

Only postive literal is H.


Some Examples of translation
----------------------------

ex 1:

To check for no duplicates in an array.

** FA is used for FOR ALL
** TE is used for THERE EXISTS

                 
                                FA(i)
                                 |
                                FA(j)
                                 |
                                 =>
                                /  \
                               =     =
                             /  \   /  \
                            a    a  i   j
                            |    | 
                            i    j



ex 2:

Array 'a' and array 'b' have the same elements.(both arrays need not have the same no. of elements)

                                       ^      
                                     /   \ 
                                FA(i)     FA(i)
                                 |          |
                                TE(j)     TE(j)
                                 |          |
                                 =          =     
                               /  \       /  \ 
                              a    b     b    a
                              |    |     |    |
                              i    j     i    j

 
ex 3:

Array 'b' is a copy of array 'a' with duplicates removed.


                                            ^
                                       /         \
                                  b has no         ^
                                 duplicates.   /       \
                                              All       All  
                                         elements of   elements of
                                         a are in b.    b are in a.

              
* and of ex1 and ex2.

ex 4:

Check for sorted array

(better soution)
                      
                               FA(i)
                                 |
                                 >=
                              /      \
                             a         a     
                             |         |
                             +         i
                            / \  
                           i   1

aliter :




                                 FA(i)
                                  |
                                 FA(j)
                                  |
                                  =>
                                /    \
                               >      >=
                             /  \    /   \
                            i    j   a    a
                                     |    |
                                     i    j


ex 5:

There is some element that occurs exactly twice in array 'a'.

                               
			        FA(i)
                                  |
                                TE(j)
                                  |
                                  ^
                               /     \
                              \=       ^
                             /  \    /    \
                            i   j   /      \
                                   =         FA(k)
                                 /   \          |
                                a    a          =>
                                |    |       /     \
                                i    j      ^        \=
                                          /  \      /  \
                                         \=    \=    a   a
                                        /  \  /  \   |   |  
                                        k  i  k  j   k   j



Ex 6:
A particular no. ,say 3, occurs same no. of times in array 'a' and aray 'b'.

For this problem it is easier to use a different approach.
In this approach array 'a' is a constant not a function.(So a(3) is not allowed.)

val(a,3)    :gives value at index 3.
count(a,3)  :counts no. of times 3 appears in a.
dim(a)      :gives dimension of array a.

For two dimensional array.

zval(b,3,5) :gives value according to index.

This problems is derived from  permutation.

ex 7:

Array 'a' is permutation of array 'b'.


                                       ^
                                     /   \
                                FA(i)     FA(i)
                                 |          |
                                 |          |
                                 =           =
                               /   \       /    \
                            count  count  count  count
                           /  \    / \     / \    /  \
                          a   val b  val  a  val  b  val
                             / \     / \     / \     / \
                            a   i   a  i    b   i   b   i


Some examples from number theory
-------------------------------

ex 8:
 
Every even no. can be written as the sum of two odd no's.


                                        FA(i)
                                          |
                                          =>
                                       /      \  
                                      ^        TE(j)
                                   /    \        |
                                   >   even    TE(k)
                                 /  \   |        |
                                i    0  i        ^
                                               /    \     
                                             odd      ^
                                              |     /    \ 
                                              j    odd    =
                                                    |    /  \
                                                    k   i   /=
                                                            / \
                                                           j   k

Exercise :

B/w any two no's 'n' and '2n' there is a prime no.