Made sure that only equivalent assertions are inserted into the context

The terms

    all(a,b) a and b => b and a

    all(a,b) b and a => a and b

are equivalent. Only one of them should be in the context.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
New prover in basic mode tested on some examples

	modified:   ocaml/context.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/prover2.ml
Added function 'is_assumption'

	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Infinite loop detection for forward reasoning

Let's assume we have the general rules

    dneg:  all(x)     x => not not x
    and_1: all(x,y)   x and y => x
    and_2: all(x,y)   x and y => y
    curry: all(x,y,z) (x => y => z) => y => x => z

> Remark: We treat `dneg` as a forward rule in order to demonstrate the loop
          breaker. But the prover does not treat `dneg` as a forward rule. But
          the same things can happen in more complicated settings

1. Loop detection with complicating forward rules (`dneg`)

Now we are in a context where we have the proved assertion

    a_1: a and b

Using `dneg` as a forward rule we get

    a_2: a and b => not not (a and b)   {dneg}

We store for each proved assertion the set of general rules which have been
used to derive them. The set of general rules here is `{dneg}`.

Now use modus ponens to derive

    a_3: not not (a and b) {dneg}

Using again `dneg` we can instantiate the forward rule

    a_4: not not (a and b) => not not not not (a and b) {dneg}

We could apply `a_3` and `a_4` with the modus ponens rule, but the prover does
not do that because in both `dneg` has been used as a general rule and `a_4`
is a complicating forward rule.

2. Allowing simplifying forward rules

Let's assume we are in a context where we have the proved assertion

    a_1: a and b and c              -- Note: `and` is left associative

We get the specific forward rules

    a_2: a and b and c => a and b    {and_1}
    a_3: a and b and c => c {and_2}

Applying modus ponens results in

    a_4: a and b {}
    a_5: c {}
       -- Note: `a_2` and `a_3` are simplifying rules. Therefore `a_4` and
       --       `a_5` do not receive the used general rules of `a_2` and
       --       `a_3`.

Because of `a_4` we get the specific forward rules by instantiating `and_1`
and `and_2`.

    a_6: a and b => a  {and_1}
    a_7: a and b => b  {and_2}

Using modus ponens we get

    a_8: a {}
    a_9: b {}

I.e. via forward reasoning the prover can split any assertion of the form
`a and b and c ...` into its elementary parts.

3. The danger of `curry`

Assume we are in a context with the proved assertion

    a_1: a => b => a and b

With that we instantiate the general rule `curry` because `a_1` matches the
premise of `curry`.

    a_2: (a => b => a and b) => b => a => a and b {curry}

and using modus ponens we get

    a_3: b => a => a and b {}   -- `a_2` is not complicating

Note that `a_2` satisfies the pattern of `curry`. This can be seen easier if
put some parentheses.

    a_2: (a => b => a and b) => b => (a => a and b) {curry}

If it were allowed to instatiate `curry` with `a_2` we would get

    a_4: ((a => b => a and b) => b => (a => a and b))
         => b
         => ((a => b => a and b)
             => a => a and b)

I have put some parentheses to see that `a_4` again matches the premise of
`curry`. So we could repeat this process ad infinitum. But the prover does not
insert `a_4` using `curry` because the general rule `curry` has already been
used in `a_2`.

	modified:   ocaml/proof_context.ml
First trial to type quantified expressions

Naively called 'boolean_term'. But a solution has to be embedded in
the structure of the typer.

	modified:   ocaml/typer.ml
Called the new prover and improved some printing functions

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/prover2.ml
Supressed printing of used forward rules

	modified:   ocaml/context.ml
Prepared new prover for backward reasoning

1. A schematic rule where the shortest tail containing all variables
   is the complete rule is no longer a backward rule because no
   premises can be extracted for backward reasoning

2. A specific rule which is an implication in not inserted into the
   backward table if there is already a backward rule with the
   same target and the same set of premises (i.e. only the order of
   the premises is different).

	modified:   ocaml/proof_context.ml
Fix: infinite loop detection for forward reasoning

The calculation if a specific rule is a simplifying forward rule
has been missing.

	modified:   ocaml/context.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
Changed 'prover local' to 'prover forward'

	modified:   ocaml/eiffelc.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/prover2.ml
	modified:   ocaml/support.ml
Removed some unnecessary consequences for the prove mode 'basic'

	modified:   ocaml/proof_context.ml
Refactored the new prover for backward reasoning

	modified:   ocaml/prover2.ml
Added structure in the new prover to break infinte backward loops

	modified:   ocaml/proof_context.ml
	modified:   ocaml/prover2.ml
Backward reasoning implemented and tested on some examples

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/prover2.ml
	modified:   ocaml/eiffelc.ml
Old prover removed from the system

	deleted:    ocaml/assertion_table.ml
	deleted:    ocaml/assertion_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/eiffelc.ml
	deleted:    ocaml/general_context.ml
	deleted:    ocaml/general_context.mli
	deleted:    ocaml/local_ass_context.ml
	deleted:    ocaml/local_ass_context.mli
	modified:   ocaml/proof_context.ml
	renamed:    ocaml/prover2.ml -> ocaml/prover.ml
	deleted:    ocaml/prover.mli
	renamed:    ocaml/term_table0.ml -> ocaml/term_table.ml
	modified:   ocaml/term_table.mli
	deleted:    ocaml/term_table0.mli
Printouts of proof tracing improved

	modified:   ocaml/context.ml
	modified:   ocaml/prover.ml
Improvements of the prover

1. Tracing functions improved (now with trace level)

2. Reduced redundancy in backward reasoning

Alternatives can be explored in an nested manner. I.e. during the exploration
of an alternative `i` for a goal `g` (using some backward rule with `g` as a
target and proving the premises) we can encounter the same goal with the same
alternatives except `i`.

If we explore at that point all alternatives different from `i` and fail we
will do the same at the original point of the alternatives.

In order to avoid this I have implemented a checker to see if down in the
stack the prover is already exploring alternatives for the same goal. In this case
it does not explore the alteratives at the top of the stack. I.e. only a breadth
search and no depth search is implemented.

3. Used schematic rules in proved terms

During backward reasoning backward rules can be applied which are not
simplifying. These backward rules are stored in the newly generated goals
(i.e. the subgoals). Therefore the subgoals can be more complicated than the
goal. If the goal is finally proved these used schematic backward rules are
stored with the proved term.

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/prover.ml
	modified:   ocaml/support.ml
Fix: Backward data have to be transformed into the context

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/prover.ml