Introduction to Artificial Inteligence

Assignment 3 - Solutions


Homework assignment - simulators, agents, search, games, logic, inference

1) Consider the following search problem over first-order logic (also known as
   LEAST-COST PROOF, which is NP-hard, even if it is known that a proof with
   a given finite n steps exists).
   You have a list KB of clauses F1,...Fk. Each Fi is of the form:

    l1 or l2 or ... lm

   where the l's are literals, i.e. an atomic sentence or its negation.
   You need to apply the operators:  a) resolution b) simplification
   in order to prove a propositional statement (by contradiction).

   Assume that applying resolution costs 1, and
   simplification costs 2 (simplification means: in a clause that contains
   2 or more instances of the same literal - remove one of them. Note that only
   ONE literal is removed at each step (e.g. reducing 3 copies of the same
   litral to 1 copy takes 2 steps).

The problem is: given clauses KB and a sentence Y, find the proof P
that has the least cost. For example, we have the KB consisting of the
clauses:
    C1:  ~P(x) or Q(y)
    C2:  ~R(x) or Q(x)
    C3:  ~Q(z)

and need to prove the sentence Y:   ~P(2) or ~R(M(1))

(hint - before the search, you need to add a transformed Y into your KB)

 a) Write the above problem as a formal search problem. Note that the
    path cost has to reflect the proof cost.

    Initial state: the given KB with the negated sentence expressed in CNF added.
    Goal test: True if the set of clauses contains the empty clause (a contradiction)
    Operators: a) Resolution applied to any 2 clauses
               b) Simplification applied to any clause
    Path cost: Total cost of operators applied along path, 2 for simplification
               and 1 for resolution.

    In the example, the initial state contains: C1, C2, C3, and the negated Y, which becomes
    TWO separate clauses: Y1': P(2)  and Y2': R(M(1))

 b) Consider the heuristic h(n) = number of literals in the shortest
    clause. Is h(n) an admissible heuristic? Prove or disprove it.

    This heuristic is admissible.
    Proof:  
     1) Exact for goal: n is a goal state iff it contains the empty clause, which has length 0,
            and thus h(n)=0 iff n is a goal state. (This claim is actually stronger than needed)
     2) Optimistic: Simplification works on only one clause, costs 2, and decreases its
          length by 1. Resolution creates a clause that is in the best case shorter by 1 than
          the shorter of the 2 clauses, and its cost is 1.
          Let h*(n) be the true cost to reach the goal. Since non of the operators decrease the
          size of the minimum cost by more than 1, the number of operators to be applied NO(n)
          in the optimal proof is at least h(n). But since each oparator costs at least 1, we
          have h*(n) >= NO(n) >= h(n).

 c) Find another another admissible heuristic h1 that performs better than h,
    for at least SOME cases (and provide an example or prove that it dominates
    h).
      
      Resolution can only decrease the length of the longer clasue if one
      of the clauses is a unit clause. Therefore, if there is no unit clause
      in the KB and no clause with duplicate literals, adding 1 to the length
      of the shortest clause still results in an admissible heuristic. Clearly
      h1 as defined here dominates h, so we need no examples...
      (Above is called "proof by intimidation".)

 d) Find a non-admissible heuristic h2 and an example where it performs better
    than h and h1.
  
    Multiplying an admissible heuristic by a large enough constant K will
    make a heuristic inadmissible. For example, making K approach infinity
    will result in A* acting like greedy search. The performance will thus
    be better every time greedy search works better than A*. An example
    is where there are many proofs of equal length, where there appears
    to be no initial headway. In this case, greedy will find a solution
    fast (sometimes even an optimal solution), while A* can take a very
    long time!

 e) Would keeping track of repeated states help in the search algorithm? If so,
    give an example.

    YES, because, for example, exchanging the steps in a proof can be possible in many cases,
    leading to the same state and with the same path cost. This can save (potentially)
    an exponential number of expansions. Example KB: A v A, B v B, ~A v ~B

    In this case we can begin by simplifying the first clause to A, or the 2nd clause to B,
    or 2 possible resolutions. Now, for the case where we simplified the 1st clause,
    we can simplify the 2nd clause, to get the KB: A, B, ~A v ~B. Likewise, for the case
    where we earlier simplified the 2nd clause, we can now simplify the 1st clause, to
    get the KB: A, B, ~A v ~B. Now from each of the KBs we have 2 possible resolutions, so
    clearly it is better to remove the redundant duplicate KB - which has the exact
    same path cost - in order to save on search!

 f) Can the algorithm be made more efficient in SPACE requirements, if
    we need to find ANY proof, rather than the shortest proof? How, and
    how much more efficient, asymptotically?

    Yes, since if we do not care about length of proof, all we need do is reach an empty clause,
    and can keep just ONE set of clauses, and just add to it all the generated clauses. That
    is because FOL is MONOTONIC.


2) For each of the following English sentences, represent them in FOL
   using the predicates given. Then, show the steps in converting them
   into conjunctive normal form.

   a) Every politician is popular in some state.
      (predicates: politician(x), popular_in(x, y), state(y))

      Forall x  politician(x) => exists y state(y) and popular_in(x, y)

      1. Remove =>

      Forall x  not politician(x) or ( exists y state(y) and popular_in(x, y))

      2,3. Move negation inwards, standardize apart - no need, already correct

      4. Move quantifiers left:

      Forall x  Exists y (not politician(x) or ( state(y) and popular_in(x, y)))

      5. Skolemize: existential y in scope of universal x, use Skolem function StateOf(x)
         Note: name of function is immaterial, as long as it is a NEW function name...

      Forall x  not politician(x) or ( state(StateOf(x)) and popular_in(x, StateOf(x)))

      6. Remove universals:

       not politician(x) or ( state(StateOf(x)) and popular_in(x, StateOf(x)))

      7. Distribute and over or (generates TWO clauses):

       a1: not politician(x) or state(StateOf(x))
       a2: not politician(x) or popular_in(x, StateOf(x))


   b) Every dog that has at least three unbroken legs can walk.
      (predicates: dog(x), can_walk(x), has(x, y), leg(y), broken(y), equality ("="))

      Forall x (dog(x) and 
                Exists y1, y2, y3  has(x, y1) and leg(y1) and not broken(y1) and
                                   has(x, y2) and leg(y2) and not broken(y2) and
                                   has(x, y3) and leg(y3) and not broken(y3) and
                                   not (y1=y2) and not (y1=y3) and not (y2=y3) ) =>
               can_walk(x)

      1. Remove =>

      Forall x not (dog(x) and 
                Exists y1, y2, y3  has(x, y1) and leg(y1) and not broken(y1) and
                                   has(x, y2) and leg(y2) and not broken(y2) and
                                   has(x, y3) and leg(y3) and not broken(y3) and
                                   not (y1=y2) and not (y1=y3) and not (y2=y3) )
               or can_walk(x)

      2. Move negation inwards

      Forall x not dog(x) or
               (Forall y1, y2, y3  not has(x, y1) or not leg(y1) or broken(y1) or
                                   not has(x, y2) or not leg(y2) or broken(y2) or
                                   not has(x, y3) or not leg(y3) or broken(y3) or
                                   y1=y2 or y1=y3 or  y2=y3 )
               or can_walk(x)

      3. Standardize apart - not needed here.
      4. Move quantifiers left:

      Forall x, y1, y2, y3         not dog(x) or
                                   not has(x, y1) or not leg(y1) or broken(y1) or
                                   not has(x, y2) or not leg(y2) or broken(y2) or
                                   not has(x, y3) or not leg(y3) or broken(y3) or
                                   y1=y2 or y1=y3 or  y2=y3
                                   or can_walk(x)
      5. Skolemize: not needed (no exsistential quantifiers)
      6. Drop universal quantifiers:
        b: not dog(x) or
           not has(x, y1) or not leg(y1) or broken(y1) or
           not has(x, y2) or not leg(y2) or broken(y2) or
           not has(x, y3) or not leg(y3) or broken(y3) or
           y1=y2 or y1=y3 or y2=y3 or can_walk(x)

      The above clause is already one (somewhat long) CNF clause, no further steps necessary.

   c) Some politicians can fool some of the people all of the time
      (predicates: politician(x), can_fool(x, y, t), person(y))

      Exists x, y politician(x) and person(x) and Forall t can_fool(x, y, t)

      1,2,3: Remove =>, move negation, standardize apart - not needed.
      4: Move quantifiers left:

      Exists x, y Forall t politician(x) and person(x) and can_fool(x, y, t)

      5: Skolemize - we have two existential variables not in the scope of universals, so
         two Skolem constants, call them POLI and FOOLED

      Forall t politician(POLI) and person(FOOLED) and can_fool(POLI, FOOLED, t)

      6: Remove universals.

      politician(POLI) and person(FOOLED) and can_fool(POLI, FOOLED, t)

      The above is three separate CNF clauses:
        c1: politician(POLI) 
        c2: person(FOOLED)
        c3: can_fool(POLI, FOOLED, t)


3) We have a search problem where the cost of each operator is 1. The branching
   factor is bounded by b. We have a heuristic evaluation function h(n) that
   is admissible, and such that h(n) >= h*(n) - 3  (that is, it is never off by more than 3).
   We use h(n) as a search heuristic in the A* algorithm.

   a) Suppose that there is only one solution to the problem. How many nodes will be
      expanded by A* using h(n) above as a heuristic, in the worst case, if
      h*(initial_state) = d  ?

      Actually, the question can be read in more than 1 way, we could have only one path
      to a solution, or multile paths to the SAME solution. We will solve this under
      both definitions, either of which constitutes a correct answer.

      If there is only one solution PATH, then every node not on this path must have
      infinite h*(n), and thus also infinite h(n), and will never be expanded. As a result,
      only d+1 nodes will be expanded.

      If solution is just the STATE (only one such solution) but many paths to the solution,
      still the number of paths is bounded due to the branching factor. But there are a LOT of ways
      of equal length in the worst case, so this number is exponential in d. In fact, it can
      be as much as b^(d+2). Henceforth we will thus assume in following questions that
      a solution is a PATH (i.e. one solution means one path).


   b) How does the above change if there is more than one solution, but any other solution
      has path cost at least 4 greater than d?

      Using the former assumption - only one optimal PATH. In this case AGAIN the number of
      expanded nodes is d+1, as follows. Let n be a node in the queue, with f(n)=g(n)+h(n),
      that is not on the optimal path. This implies n is either on a non-solution path,
      and has infinite h(n) (thus never expanded), or is on the optimal path to some other solution
      g, with g(g) => d+4. Now, f(n) =g(n) + h(n) >= g(n) + h*(n) - 3 = g(g) - 3 > d.
      This means that n will never be expanded, because the optimal node g* will be expanded
      earlier.

   c) Same as in (b), but there is also ONE solution with cost d+2.

      In this case, nodes on the path to the secondary goal may also be expanded, and
      in fact all the nodes on that path up to but not including the secondary goal
      may be expanded in the worst case. Total expansions would be: 2d + 3.
     


4) Consider the stochastic game to be implemented in assignment 2: grid based environment,
   agents can move forward, turn right or left, and shoot (hitting with probability p/d, where
   d is the distance). You may assume a time limit as desired for the length of the game in
   each scenario.

   a) Show a scenario (with no bullets) where for the first agent to move, under zero-sum scoring,
      moving forward loses, but under total flags collected scoring the optimal move is to move forward.

      Consider the following scenario, with agent A to move, and where the game ends after
      a time limit of 6 ply (3 moves by each agent).

       +------+------+------+------+
       |  F1  |  F2  |  A   |      |
       |  (1) |  (1) | <--  |      |
       |      |      |      |      |
       +------+------+------+------+
       |  B   |      |   F3 |  F4  |
       | -->  |      |  (1) | (10) |
       |      |      |      |      |
       +------+------+------+------+

       Observe that without opposition, B can reach either F1 or F3 and F4, but A can only reach F1 and
       F2 (by moving forward) or F3. If A moves forward, then B will be able to reach the F3 and F4
       flags, and under zero-sum scoring the score will be at best -9 for A. Therefore, the best action
       for A is to turn left and then take F3, in which case B will take F1 for a total score
       difference of 0.

       However, under total flags collected scoring, A should move forward in order to collect
       F2 and F1 for a score of 2, allowing B to collect F3 and F4 for a score of 11.


   b) In the game with bullets, show a scenario where the the first agent to move loses.

       +------+------+------+
       |      |  F   |      |
       |      | (1)  |      |
       |      |      |      |
       +------+------+------+
       |  B   |      |  A   |
       | -->  |      | <--  |
       |      |      |      |
       +------+------+------+
       |      |  F   |      |
       |      | (1)  |      |
       |      |      |      |
       +------+------+------+

      Suppose that A is to move, and p=1 and k=1. There are 4 possibilities here:

      A: Forward loses - score is -2 because then B shoots and kills A, and can then
            get both flags. No need for search to prove this.
         Turn left or right loses (consider just one of them, due to symmetry):
           B: Shoots. This has two outcomes, each with probability 0.5
               A dies, and then B collects flags to get score of 2 (i.e. -2 for A)
               A lives, and then:
                    A: Forward to collect a flag, and gets it, but B can get the other flag
                       (score here is 0).
                    A: Turn left (in order to shoot).
                       B: Turn right (or left, which is the same) in order to run and collect a flag.
                            A: Shoots, and then with probability 0.5:
                                B dies, and A scores 2, or -2 for B.
                                B lives, and can then collect 1 flag (score 0).
                              (expected score here is 1 for A).
                       B: forward (A shoots and score is 2 for A)
                       (So in the case B should turn, and expected score is  1 for A).
                    A: Other actions: score of 0 for A (each collects a flag).
                    (Best action for A is thus turn left, expected score 1).
               (Expected value of B's shot is thus -0.5 for A and 0.5 for B).

Since the scenario is symmetric, if B moves first then B's expected score is -0.5,
i.e. the first player to move is expected to lose!)

   In both cases, you must PROVE the scores by generating the respective game tree, either
   to a terminal position or prove that you can prune some branches.
   

   c) Suggest heuristic evaluation functions for the total-flags scoring version of the game:
     1) One that is a lower bound, but non-trivial.

          A trivial lower bound is value of flags already collected.
          To that, we can safely add value of flags in partial spanning tree with cost
          that is less than half the manhattan distance between agent A and agent B
          (so  that B will not be able to block A).

     2) One that is optimistic an upper bound, but non-trivial

          A rather trivial upper bound is value of flags collected plus value of all
          remaining flags. From this we can safely subtract the values of flags the opposing
          agent can reach before we can reach them (or block the opponent), that is,
          the part of the spanning tree for the opponent with total distance less than half
          the manhattan distance between agent A and agent B (so that we cannot collect these
          flags before the opponent, and cannot block its way).


5)  Completing the proof from wumpus world done in class, plus a bit more...
    a) Write the following domain axioms in FOL:
       1. A wumpus stinks up all ajacent squares. ("square" and "location" are used interchangably here)

          Forall l1, l2   Wumpus(l1) and Adjacent (l1, l2) => Stinky(l2)

            (also need to restrict l1 and l2 to be legal locations, but we can do that in
             the requirements for "Adjacent")

       2. Only at most one square contains a wumpus. (This is a new one, to make it interesting).

          Forall l1, l2  Wumpus(l1) and Wumpus(l2) => l1 = l2

            (Note that although these should also be Legal locations, we can ignore
             this requirement for our limited application)

       3. A stinky square implies a wumpus in an adjacent square.

          Forall l1, l2  Stinky(l1) => Exists l2 Wumpus(l2) and Adjacent(l1, l2)

       4. Zero is an integer, and a successor of an integer is an integer.
          (We need to add an "Integer" predicate in order to encode this).

           Integer(0) and (forall x Integer(x) => IntegerS(x))

       5. The successor of 0 is 1, ... the successor of 3 is 4...
           S(0) = 1  and S(1) = 2 and S(2) = 3 and S(3) = 4

       6. An integer is greater-than-or equal to itself, and a successor of an
         integer x is greater-than-or-equal to x.

           Forall x (x >= x) and (S(x) => x)

       7. The value of the function first(x) is the first element of x.

          Forall x, y   x = First([x, y])

       8. The value of the function second(x) is the second element of x.

          Forall x, y   y = Second([x, y])

       9. Squares (locations) are adjacent if and only if they have one coordinate
          equal to the other, and in the other coordinate one is the successor of
          another, and both are legal.

          Forall x1, x2, y1, y2  Adjacent([x1, y1], [x2, y2])    <=>
               (Legal([x1, y1]) and Legal([x2, y2]) and
                ((x1=x2 and (y1 = S(y2) or y2 = S(y1))) or
                 (y1=y2 and (x1 = S(x2) or x2 = S(x1)))))

      10. A square (location) is legal if and only if its first and second
          coordinates are between 1 and 4.

          Forall x, y   Legal([x, y]) <=> 
             (Integer(x) and Integer(y) and x >= 1 and 4 >= x and y >= 1 and 4 >= y)

      11. A location with no wumpus is safe.

          Forall x, y  not Wumpus([x, y]) => Safe([x,y])

         The predicates to use are:
            Wumpus(loc), Legal(loc), Adjacent(loc1, loc2), Stinky(loc), Safe(loc), x=y, x >= y
         Constants to be used are: 0, 1, 2, 3, 4, 5, ...
         Functions to be used are: S(x), First(x), Second(x).

     b) Convert the above into conjunctive normal form, this is your basic KB.
       1.  not  Wumpus(l1) or not  Adjacent (l1, l2) or Stinky(l2)

       2.  not  Wumpus(l1) or not Wumpus(l2) or l1 = l2

       3a. not Stinky(l1) or Wumpus(WumpusLocationFor(l1))
       3b. not Stinky(l1) or Adjacent(l1, WumpusLocationFor(l1))

          (Using a Skolem function of one argument WumpusLocationFor(l1))

       4a. Integer(0) 
       4b. not Integer(x) or Integer(S(x))

       5a.  S(0) = 1
       5b.  S(1) = 2
       5c.  S(2) = 3
       5d.  S(3) = 4

       6a. x >= x
       6b. S(x) => x

       7. x = First([x, y])

       8. y = Second([x, y])

       Due to complicated and/or structure, 9 breaks up into quite a number of CNF clauses:

       9a. not Adjacent([x1, y1], [x2, y2]) or Legal([x1, y1])
       9b. not Adjacent([x1, y1], [x2, y2]) or Legal([x2, y2])
       9c. not Adjacent([x1, y1], [x2, y2]) or x1=x2 or y1=y2
       9d. not Adjacent([x1, y1], [x2, y2]) or x1=x2 or x1=S(x2) or x2=S(x1)
       9e. not Adjacent([x1, y1], [x2, y2]) or y1=y2 or y1=S(y2) or y2=S(y1)
       9f. not Adjacent([x1, y1], [x2, y2]) or x1=S(x2) or x2=S(x1) or y1=S(y2) or y2=S(y1)
       9g. Adjacent([x1, y1], [x2, y2]) or not Legal([x1, y1]) or not Legal([x2, y2])
             or not x1=x2 or not y1=S(y2)
       9h. Adjacent([x1, y1], [x2, y2]) or not Legal([x1, y1]) or not Legal([x2, y2])
             or not x1=x2 or not y2=S(y1)
       9i. Adjacent([x1, y1], [x2, y2]) or not Legal([x1, y1]) or not Legal([x2, y2])
             or not y1=y2 or not x1=S(x2)
       9j. Adjacent([x1, y1], [x2, y2]) or not Legal([x1, y1]) or not Legal([x2, y2])
             or not y1=y2 or not x2=S(x1)

      Same goes for 10:

      10a.  Legal([x, y]) or not Integer(x) or not Integer(y) or not x >= 1 or not 4 >= x or
                             not y >= 1 or not 4 >= y
      10b.  not Legal([x, y]) or Integer(x)
      10c.  not Legal([x, y]) or Integer(x)
      10d.  not Legal([x, y]) or x >= 1
      10e.  not Legal([x, y]) or 4 >= x
      10d.  not Legal([x, y]) or y >= 1
      10d.  not Legal([x, y]) or 4 >= y

      11.  Wumpus([x, y]) or Safe([x,y])

     c) Add the following to the basic KB: 

       13. not Stinky([2,1])
        Prove by refutation (using just resolution) that Safe([2,2]).

         We add the negation (already a single clause):
 
      14. not Safe([2,2])

      And now we can start the proof. 14 resolves with 11, {x/2, y/2} to get:

      15.  Wumpus([2,2])

      Resolving 15 with 1, {l1/[2,2]} we get:

      16.  not Adjacent([2,2], l2) or Stinky (l2)

      Resolving 16 with 13, {l2/[2, 1]} we get:

      17. not Adjacent([2,2], [2,1])

      Resolving 17 with 9g, {x1/2, y1/2, x2/2. y2/1} we get:

      18. not Legal([2, 2]) or not Legal([2, 1]) or not 2=2 or not 2=S(1)

      Here we find that we are missing axioms fr equality! Let us have:

      =a.  x=x                        (= is reflexive)
      =b.  not x=y or y=x             (= is symmetric)
      =c.  not x=y or not y=z or x=x  (= is transitive)

      Now, resolving 18 with =a, {x/2} we get:

      19. not Legal([2, 2]) or not Legal([2, 1]) or not 2=S(1)

      Resolving 19 with =b, {y/2, x/S(1)} we get:

     20.  not Legal([2, 2]) or not Legal([2, 1]) or not S(1)=2

      Resolving 20 with 5a:

     21. not Legal([2, 2]) or not Legal([2, 1])

     Now, let us assume for simplicity that we have already added the sentences Lij: Legal([i,j])
     (see appendix on how this is done).

     Resolving 21 with L22 we get:

     22. not Legal([2, 1])

     and finally, resolving 22 with L21 we get the empty clause, which proves
     the "theorem" Safe([2, 2]) by contradiction.


     d) In addition to the above, add to the KB: Stinky([3,1]) and Stinky([2,2]).
        Prove by refutation (using just resolution): Safe([1,2]).

        We begin by adding:

        D1:  Stinky([3,1])
        D2:  Stinky([2,2])

        And then in order to begin the proof, we add the negation of the query:

        Q2: not Safe([1,2])

        Now we can begin, resolving Q2 with 11, {x/1, y/2} to get:

        D3: Wumpus([1,2])

        Resolve D3 with 2, {l1/[1,2} to get:

        D4: not Wumpus(l2) or [1,2] = l2

        Now we resolve D1 with 3a, {l1/[3,1]} to get:

        D5: Wumpus(WumpusLocationFor([3,1])

        Likewise, we resolve D1 with 3b wo get:

        D6: Adjacent([3,1], WumpusLocationFor([3,1]))

        Resolve D5 with D4, {l2/WumpusLocationFor([3,1])} to get:

        D7: [1,2] =  WumpusLocationFor([3,1])

        We are missing YET ANOTHER equality axiom, which is:

        EE: not Adjacent(l1, l2) or not l3=l2 or Adjacent(l1, l3)

        Resolve EE with D6, {l1/[3,1], l2/WumpusLocationFor([3,1])} we get:

        D8: not l3=WumpusLocationFor([3,1]) or Adjacent([3,1], l3)

        Resolve D8 with D7, {l3/[1,2]} to get:

        D9: Adjacent([3,1], [1,2])

        Now, resolve D9 with the 9c axiom for adjacency, with {x1/3, y1/1, x2/1, y2/2} to get:

        D10: 3=1 or 1=2

        Now we are missing some MORE trivial axioms, for example we need to know that not 3=1,
        etc. Let us assume that we already have axioms NEij for all such cases...
 (This is a lot of axioms! however we can start with: 
        NE:  not S(x) = x
        NE': not S(x) = y or not x >= z or not  y=z
        EQ': not y=x or y=z or not x=z

        And from these we can quickly get what we need, e.g. resolving EQ' with 5b,
        with {y/S(1), x/1} we get:
           S(1)=z or not 2=z 
        Resolving the latter with NE, {x/1, z/1} we get:
        NE10:  not 2=1
        In this way we can show all the required inequalities NEij.
)

        Now, we can finally resolve D10 with NE31 followed by resolving the result with NE12 to
        get the empty clause!
                   

----------------------------------------------------------------------------------------------        
Appendix: we need to prove the statements Lij: Legal([i, j]) for some of the i, j in
     order to complete the proofs. Note that this is NOT query dependent, in the sense
     that we can do it for all integer i, j greater than 0 and less than 5. But we don't need
     ALL of them here, just the ones for the actual queries. Nevertheless, below is the
     method to obtain them by resolution.

     First, we generate the required integers and their comparative size. We need additional
    axioms for equality (these could be avoided with an inference rule treating equality in
    a special way that allows unification up to equality):

    I1:  not Integer(x) or not x=y or Integer(y)
    I2:  not (S(x) >= x) or not  (S(x) = y)  or y >=x

    Resolving 4a with 4b, {x/0} we get:

    A1: Integer(S(0))

    Resolving A1 with I1, {x/S(0)} we get:

    A2: not S(0) = y or Integer(y)

    Resolving A2 with 5a, {y/1} we get:

    A3: Integer(1)

    In a similar wa we resolve A3 with 4b, then with I1, then with 5b, to get,

    A4: Integer(2)

    And likewise:

    A5: Integer(3)

    Now we need to prove some auxilliary i => j statements.
    Resolving 6b with I2, {x/x, y/2} we get (note wierd notation - we actually should have
    had a different variable, say x', instead of x in I2, and then the substitution would
    have been: {x'/x, y/2}):

    A6: not (S(x) = y) or y >= x

    Now we resolve A7 with 5b, {x/1, y/2} to get:

    A8: 2 >=1

    Resolving A6 with 5c, {x/2, y/3} we get:

    A9: 3 >=2

    And resolving A6 with 5d, {x/3, y/4} we get:

    A10: 4 >= 3

    We now also need transitivity of =>:

    GE: not x=> y or not y=>z or x=>z

    Resolving GE with A8 then the result with A9, unifiers {y/2, z/1} and {x/3} respectively, we get:

    A11: 3 >= 1

    Likewise resolving GE with A9 and A10 we get:

    A12: 4 >= 2

    And resolving GE with A12 and A8 we get:

    A13: 4 >= 1

    Now we can try to prove some Legal([i,j]) statements. For example, resolving 10a
    with A4, {x/2} we get:

    A14: Legal([2, y]) or not Integer(y) or not 2 >= 1 or not 4 >= 2 or not y >= 1 or not 4 >= y

    Resolving A14 with A8 and A13 we get:

    A15:  Legal([2, y]) or not Integer(y) not y >= 1 or not 4 >= y

    Resolving A15 with A3, {y/1} we get:

    A15:  Legal([2, 1]) or not 1 >= 1 or not 4 >= 1

    And finally resolving A15 with 6a, {x/1} and then with A13 we get:

    L21:  Legal([2, 1])

    In a similar way we can resolve A14 with A4, {y/2} to get: 

    A16:  Legal([2, 2]) or not 2 >= 1 or not 4 >= 2

    And then resolve A16 with A8 followed by resolution with A12 to get:

    L22:  Legal([2, 2])

    Likewise for all the othe Lij statements we need...