Algorithm Alley
by Sergei Savchenko


Example 1:
(a)

(c>'1')A = c e : 2 2 : 3 3 :

(b)
A= c e : 1 1 : 1 2 : 2 2 : 3 3 :
B= x y : 1 9 : 2 8 : 4 9 :
<A[cx]B>= c e y : 1 1 9 : 1 2 9 : 2 2 8 :

(c) 
(c>'1')<A[cx]B>= c e y : 2 2 8 :


Listing One
Step 1: Remove - and = 
    g-h is substituted by ~g|h
    g=h is substituted by (~g|h)&(g|~h)

Step 2: Distribute negation so only atoms are negated
    ~(g|h) is substituted by ~g&~h
    ~(g&h) is substituted by ~g|~h

Step 3: Distribute ors over ands
    g|(h&f) is substituted by (g|h)&(g|f)
    (h&f)|g is substituted by (h|g)&(f|g)

Listing Two
(~(a-b))|c        (Eliminating "-");
(~(~a|b))|c       (Distributing not);
(a&~b)|c          (Distributing | over &);
(a|c)&(~b|c)      (Obtaining clauses).

Listing Three
Statement:              CNF:                     Clauses:
---------------------------------------------------------------------
k                       k                        (0) k
(~a-b)                  (a|b)                    (1) a|b
(k-l)                   (~k|l)                   (2) ~k|l
((b&l)-a)               ((~b|~l)|a)              (3) ~b|~l|a
~a                      ~a                       (4) ~a

Proof:
---------------------------------------------------------------------
(0) k
(1) a|b
(2) ~k|l
(3) ~b|~l|a
(4) ~a
(5) ~b|~l from (4) and (3)
(6) ~b|~k from (5) and (2)
(7) ~k|a from (6) and (1)
(8) ~k from (7) and (4)
(9) contradiction from (8) and (0)

Listing Four
Statement:              CNF:                     Clauses:
---------------------------------------------------------------------
{e(x)-o(p(x))}          {~e(x)|o(p(x))}          (0) ~e(x)|o(p(x))
{o(x)-e(p(x))}          {~o(x)|e(p(x))}          (1) ~o(x)|e(p(x))
~{e(a())-e(p(p(a())))}  {e(a())&~e(p(p(a())))}   (2) e(a())
                                                 (3) ~e(p(p(a())))
Proof:
---------------------------------------------------------------------
(0) ~e(x)|o(p(x))
(1) ~o(x)|e(p(x))
(2) e(a())
(3) ~e(p(p(a())))
(4) ~o(p(a())) from (3) and (1)
(5) ~e(a()) from (4) and (0)
(6) contradiction from (5) and (2)

Listing Five
Relations:
---------------------------------------------------------------------
A = x : 1 : 2 : 3 : 4 : 5 :
B = y : 1 : 5 : 7 :

Statement:              CNF:                     Clauses:
---------------------------------------------------------------------
a(.x)@A                 a(.x)@A                  (0) a(.x)@A
b(.y)@B                 b(.y)@B                  (1) b(.y)@B
{{a(x)&b(x)}-l(x)}      {{~a(x)|~b(x)}|l(x)}     (2) ~a(x)|~b(x)|l(x)
~l(y)                   ~l(y)                    (3) ~l(y)

Result:
---------------------------------------------------------------------
A= x : 1 : 2 : 3 : 4 : 5 :
B= y : 1 : 5 : 7 :
(0) a(.x) @ A
(1) b(.y) @ B
(2) ~a(x)|~b(x)|l(x)
(3) ~l(y)
(4) ~a(x)|~b(x) from (3) and (2)
(5) ~a(.y) from (4) and (1) @ B
(6) contradiction from (5) and (0) @ <B[yx]A>
<B[yx]A> = y : 1 : 5 :

Listing Six
Relations:
---------------------------------------------------------------------
A= c e : 1 1 : 1 2 : 2 2 : 3 3 :
B= p s t : 1 a p : 2 a t : 2 b t : 2 c p : 3 c t :

Statement:              CNF:                     Clauses:
---------------------------------------------------------------------
{e(.e)-c(.c)}@A         {~e(.e)|c(.c)}           (0) ~e(.e)|c(.c)@A
t('t')                  t('t')                   (1) t('t')
{{c(.p)&t(.t)}-s(.s)}@B {{~c(.p)|~t(.t)}|s(.s)}  (2) ~c(.p)|~t(.t)|s(.s)@B
~{e('3')-s(x)}          {e('3')&~s(x)}           (3) e('3')
                                                 (4) ~s(x)
Result:
---------------------------------------------------------------------
A= c e : 1 1 : 1 2 : 2 2 : 3 3 :
B= p s t : 1 a p : 2 a t : 2 b t : 2 c p : 3 c t :
(0) ~e(.e)|c(.c) @ A
(1) t('t')
(2) ~c(.p)|~t(.t)|s(.s) @ B
(3) e('3')
(4) ~s(x)
(5) ~c(.p)|~t(.t) from (4) and (2) @ B
(6) ~c(.p) from (5) and (1) @ (t='t')B
(7) ~e(.e) from (6) and (0) @ <(t='t')B[pc]A>
(8) contradiction from (7) and (3) @ (e='3')<(t='t')B[pc]A>
(e='3')<(t='t')B[pc]A> = e p s t : 3 3 c t :






3


