no more prove in palette

fixed or-in-left

fixed not-e

Another bug.

This commit shows a bug.

almost ready

rules fixed

make all/clean implemented

housekeeping

housekeeping

house keeping

disambiguation can use a goal as hint for the expected type

natural deduction palette

test 4 luo

...

better names

disambiguation for ng terms almost there

some new exports

new meta added for ng_disambiguation

exported disambiguate_thing

occurr check fixed

more printings

last fixes

1. data structure for lables is now more strict
2. phase 3 completed (with a test)
3. simple optimizer for redundant jumps implemented

- we now use a streaming architecture (run time gain: 11 secs)
- we added some time stamp support

auto-param "size" missing

debug=false

Signature_of has been closed with respect to constructors.

The signature in "retrieve equations" must be extended with the equality if
not already there, otherwise it may hardly find any equation.

some other simplification

ordered_set simplified

exercise ready

exercise ready

almost there

...

First attempts at the third phase.

added some news

almost ok

natural deduction support and example split, seems to almost work.

do not erase sorts

better error messages. sorts are compared using whd

Evil case fixed, the coulde should be more readable

removed empty lines

the passive set and passive list are expected to have the same cardinality, that was was some bad reason not always the case

fixed scripts

still some glitches, but reaching a decent state

using the new by foo we proved semantics

new internal flags for auto:
- skip_context
- skip_trie_filtering

together they allow a decent semantics for
by H, H1, H2 we proved foo.

since only H, H1 and H2 are used (no other context entry, not library stuff)
and full blown unification is used (no terms are ignored, between the one
specified, because they fail a trie search)

duplicate entry in menv avoided

fixed script to use auto depth=4

eliminazione di un passaggio di transitività in ast2astfe
dimostrazione di un assioma in env2flatenv

Calling unification instead of matching when checking for subsumption
might instantiate the goal with variables in table (while they are supposed
to be disjoint).

- A new interesting elimination principle over inductively generated topologies:
  the elimination principle for general topologies hold!
- A proof of Cantor theorem using formal topologies. By Silvio Valentini.

BDD

removed prerr_endline

debug=false

shannon proved

added shannon

added lazy

Environment simplified.

No longer used.

- New dependency for environments on the nesting depth.
- New invariant that tightly binds the list of identifiers in scope with
  the list of mappings in an environment transformation map
- Second pass of the compiler finally complited

Propagation of changes in paramodulation.

Exported a couple of functions.
--Thi sline, and those below, will be ignored--

M    metadataQuery.mli

Added a in_universe function

propagation of changes in other paramodulation files.

New demod function working for arbitary goals.

models ported

Enforcing the disjoint invariant between metasenvs.

Main change: added a parameter to build_equality_proof to discriminate
bewteen forward and backward rewriting steps.

even more polymorphic dualizer

done

...

lebesge works

WIP

many bugs fixed

metasenv passed to get_relevance, Metas that stand for sorts have shift 0 and len 0

WIP

_ in place of unused variables

Implicit annotationas are now printed

seg_u/l were inverted, more work

big lemma done

...

duality done

almost done, just needs to be prforated

....

all done in declarative style

...

...

duality is a joke

...

leave-environment axiom made true

lebesgue completely dualized

we aligned the implementation to the plmms08 paper

...

better pps

- mk_restricted_irl removed, the non-optimized code was the same
- delift fixed in case Meta (used to produce negative shift/irl-len)
- fix-sorts takes into account the swap parameter to implement cumulativity

psubst for metas fixed again

nat model ported to the dualized version, but not itself dualized dedekind-sig-compl missing

... is a command in proof mode, use
\ldots instead