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

better output handling

return type of paramod fixed according to the SZSOntology

...

...

Version number set to 1.0.0-rc1

Fixed type of bag

parallel

Moved ID management inside the bag

attempt of using 2 different orderings

....

Corrected a few typos

...

Enabled age selection (ratio 1/5)

lambda-delta:
- lib/output: infrastructrure for reduction reporting
  we found just one instance of "referene typing" in the "Grundlagen"
  rt.txt reports where it occurs
- lib/time: bugfix
- basic_rg: bugfix (some relocations were missing)
  the "Grundlagen" now typechecks :)

...

do not infer on closed goals

removed a maybe diverging test

...

First attempt for refined goal selection strategy

added (but not active) last chance idea

Implemented orphan murdering technique

new make test target

new kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes

attempt to run a last chance procedure after the timeout

the timeout is passed to test last chance

this case is not assert false since it can happen if occur_check
makes fail the unification

fixed parsing

convenient problem lists

an easy for loop

deep subsumption activated

test for deep subsumption added

Implemented orphan murder test (clauses are not discarded for now)
Re-enabled zero weight trick

...

better doc

timeouts are passed as arguments, so that tptpprover can
accept --timeout argument. Moreover it prints the proof
according to the SZS ontology

- some depend files :)

the prover is almost OK, types in fuctors a bit extended to
ease their instantiation

First version of deep_subsumption.

Various fixes

new function

...

matitaprover is almost there

...

initial import of standalone matitaprover binary

Now using age selection

code refactoring for paramodulation

new function list_mapi_acc

Fixed is_identity for facts

Fixed insertion of passive clauses

Code factorization

Removed debug printing

Now inserting hypothesis and goal with zero weight

Extended is_identity test
First step towards age selection

Implemented check for duplicates (in goals)

Removed old debugging assertion

- procedural: basic support for lapply (solves a problem in the reconstruction of algebra/groups.ma)
- lambda-delta: bugfix in line counts and nodes counts

Removed debug printing raising Failure

Removed debug printing

Rewrote the main loop for paramodulation

undo/serialization for universes implemented

Debugging prerr_endlines removed.