Fixed typo

Ported innermost strategy for demodulation from trunk

Fixed (yet another) nasty bug, in deep_eq this time

Fixed nasty bug in superposition and freshing of clauses

Now iterating superposition

Ported demodulation on clauses

Added check for trivial (identity) goal

Update eligible problem list (now sorted)

Added TreeLimitRun

Added Clauses module

Added symbolic link to clauses

Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertible (in orderings)

Various architectural changes

Various architectural changes

Added symbolic links to hTopoSort

Fixed pretty printer and debug printings

First compiling version

Fixed useage

Fixes

Fixed conflicts due to problem when merging with UEQ implementation

Branched paramodulation for CNF (Horn clauses)

ncopy partially implemented and fixed (a ?) chain to print elimintaors

Fixed dependency function, which was lacking the code for recursive calls.

...

match_coercion gives back the saturations, not the arity:
`f ??????? x ???? y z` has to be rendered as `x y z`
   <----->   <-->
    cpos     stat

 freescale porting, work in progress

Fixed Option type error (OCaml bug)

.

.

 freescale porting to ng, work in progress

better spacing

statistics are used, when possible, to sort
constants

Added statistics printings

Added statistics module

First proof finished (some tactics still not working).

matitaprover is now flexible enough to allow the computation of statistics on
the clauses and then choose an ordering to be used for the proof search

Coercion hiding implemented. Notes:

1) hiding of coercions whose return type is a product is not done correctly,
   since the "sats" information seem to have changed semantics. Enrico, is it
   a bug or just a new semantics?
2) coercion matching has been implemented trivially (O(n)) in NCicCoercion.
   Here I need a special version of a discrimination tree. Enrico, do we have
   one already or is there a way to simulate it?

 freescale translation (work in progress)

Composite coercions are here!

- brgOutput: the nodes count is now implemented
- brgReduction: the type annotation in the beta-reductum is useless
- brgType: a never-occurring condition marked with assert false

initial implementation of coercion composition

more work on coercions composition

 +root +depends

Removed unused parameter of unification procedure (vars)

more profilers

Coercions used here and there.

Bug fixed (missing ctx) + comment added.

...

new ng freescale, no external dependencies

Let's live with new ocaml type system limitations...

initial implementation of `ncoercion name : type := body on name : pat to pat`

claudio, please have a look at this

new nrepeat (and block '('...')' ) tactical

...

New functorialization: paramod is abstracted over a Orderings.Blob, that is like Terms.Blob but adds the compare_terms function.
This allows an easy instantiation of the main loop with differend orderings

Fixed check for condition iv p.33 (Riazzanov)

More updates to Fsub.

profile most operations, do not return a filtered varlist in unif (useless and expensive)

1 process for now

two cases should be assert false at least in TPTP

micro optimizations to unification

Cleaned a bit

...

activate kbo, not lpo

...

Bug fixed (non-captured variable).

eq moved to CProp
In Prop a unification problem was not solved, but I suspect that that was
a bug...

...

repeat_tac

...

few more files, one diverges

directory for porting the assembly to matita-ng

removed useless universes

import of a sample for cosimo

Hmmmm. This way we need "canonical structures" also for local definitions => BAD

...

Metavariable case in does_not_occur (hence weakly/stricly, positive, etc.)
relaxed. Is this always correct??

Missing case for Match implemented.

...

weakly/strictly positive checks relaxed to allow metavariables that are not
substituted

...

Improved error message.

Bug fixed: the debrujinate function (hence the one to compute objects height)
did not take the substitution.

...

Bug fixed: one uri was not refreshed, causing divergence of the kernel!

fixed some typos

Let's play a bit with NG.
This library is NOT meant to be the final one, just a way to experiment with
features.

1) Include files for NG were neither recursively processes nor accumulated.
   They are now recursively processed (is this the best solution???)
2) Bug fixed (an assertion raised in including an included file because of
   a false assertion on references)

Fixed printing of number of problems solved

Tried to implement lpo in a more efficient way

Fixed typo in lpo (from old implementation)

some corrections

more static analysis on the Automath text

Ported old implementation of LPO (for test purposes)

we now do some static analysis on the Automath text to possibly clear some language ambiguities

Implemented LPO

Corrected type for bag

New age selection
New demodulation strategy