Some clean up and explicit "not yet implemented" error messages

	modified:   ocaml/class_table.ml
	modified:   ocaml/feature_table.ml
Minor bugfix in calculating de Bruijn indices

	modified:   ocaml/feature_table.ml
	modified:   ocaml/term.ml
Minor edit
Splitted assertion_table into assertion_table and prover

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/eiffelc.ml
	renamed:    ocaml/assertion_table.ml -> ocaml/prover.ml
	new file:   ocaml/prover.mli
Prover finds exact matches of the current goal in the global assertion table

This is done via unification and by looping through all assertions in the
assertion table. The algorithm needs improvement in the future because
it is not very efficient.

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/class_table.ml
	modified:   ocaml/proof.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml
Prover does backward reasoning with the global assertion table

Suppose that the prover wants to prove a goal 'goal' and in the global
assertion table we have the proved assertion

    all(a:BOOLEAN) not not a => a

then the prover loads 'not not goal => goal' into the context. Since
the proved assertion 'not not a => a' is not simplifying in backward
direction a detector is implemented which checks that such a non
simplifying formula cannot by applied repeatedly. Without the
detector the prover would load

    not not goal => goal
    not not not not goal => not not goal
    not not not not not not goal => not not not not goal
    ...

by its backward reasoning engine into the context.

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/container.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml
Reworked backward reasoning with global assertion table

Backward reasoning with non simplifying rules seem to cause enormeous
combinatorial complexity even if a loop detector is implemented.

Therefore backward reasoning is now restricted to work only if all
subgoals are not more complex (in terms of node count) than the goal
to be proved (provisions are still pending to allow for distributivity).

With this restriction the proof engine works quite fast and good.

The restriction has the disadvantage that the user has to indicate
if he wants an indirect proof (i.e. if he wants to prove 'a' by
assuming 'not a' and deriving a contradiction).

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/container.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
Forward reasoning with global assertion table implemented

If the assertion table has a proved assertion of the form a=>b and
the context of the prover contains an assertion u which can be unified
with a and the unified variables are sufficient to transform b to an
expression v valid in the environment of u (and v is not more complicated
than u) then u=>v can be added to the context. The local forward engine
of the prover proves then v automatically.

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/prover.ml