Redesign of the prover

- Does forward reasoning only if the final target is simpler than the most
  complex premise (including already consumed premises).

- Allows partial specialization in general.

- Allows backward reasoning for 'catchall' targets if the rule has already
  been partially specialized and used at least once in forward direction
  (i.e. the first premise already dropped).

- Stores all proved assertions in prenex normal form with respect to universal
  quantification.

- Does not store assertions in the search tables if they are implications
  which are immediately used to apply the modus ponens rule.

The restriction of forward reasoning has been necessary because the original
strategy (which allowed forward reasoning if the final target is not more
complicated than all premises) together with partial specialization created a
lot of useless terms in the context.

Partial specialization is useful e.g. for the rules

    all(a,b,c) a or b ==> (a ==> c) ==> (b ==> c) ==> c

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

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

which result in the following partial specializations if the first premise is
in the context

    all(c) (a ==> c) ==> (b ==> c) ==> c

    all(p) p(a) ==> p(b)

    all(c) b = c ==> a = c

The first one has a 'catchall' target and therefore triggers a case split for
any goal, i.e. it proves the goal by first assuming `a' and then assuming
`b'.

The second rule can be used to prove any predicate on `b' by proving the same
predicate on `a'. The rule is used in forward direction as long as `b' is
simpler than `a'

The third rule can be used to prove that `a' is equal to any term by proving
that `b' is equal to the same term. The rule is used in forward direction if
`a' is simpler than `b'.

Prenex normal form guarantees that the proved rule

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

is stored in the form

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

which makes it applicable for partial specialization. The first one would never
be applied in forward direction because the target is not simpler than the
premise. The second one can at least be partially specialized. Further
reasoning then depends on the complexity of `a' and `b'.

	modified:   ocaml/alba.ml
	modified:   ocaml/ast.ml
	modified:   ocaml/container.ml
	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/proof.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/prover.ml
	new file:   ocaml/rule_data.ml
	new file:   ocaml/rule_data.mli
Catch all rules deactivated

Catch all rules are possible as backward rules on any target. The
current implementation of the prover can cause combinatorial
explosion in the presence of more than one catch all rule.

In case of failure it tries the catch all rules in all possible
permutations. Before activating catch all rules again a solution
has to be found to avoid this combinatorial explosion.

	modified:   ocaml/rule_data.ml
Equality tables added to the proof context

	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/rule_data.ml
	modified:   ocaml/term.ml
New structure introduced for beta reductions and function expansions

The structure is tested but not yet used.

	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli