]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years agofew more files, one diverges
Enrico Tassi [Wed, 8 Jul 2009 14:09:06 +0000 (14:09 +0000)]
few more files, one diverges

15 years agodirectory for porting the assembly to matita-ng
Cosimo Oliboni [Wed, 8 Jul 2009 10:03:08 +0000 (10:03 +0000)]
directory for porting the assembly to matita-ng

15 years agoremoved useless universes
Enrico Tassi [Wed, 8 Jul 2009 09:58:29 +0000 (09:58 +0000)]
removed useless universes

15 years agoimport of a sample for cosimo
Enrico Tassi [Wed, 8 Jul 2009 09:56:26 +0000 (09:56 +0000)]
import of a sample for cosimo

15 years agoHmmmm. This way we need "canonical structures" also for local definitions => BAD
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 03:30:52 +0000 (03:30 +0000)]
Hmmmm. This way we need "canonical structures" also for local definitions => BAD

15 years ago...
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 02:36:19 +0000 (02:36 +0000)]
...

15 years agoMetavariable case in does_not_occur (hence weakly/stricly, positive, etc.)
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 02:36:08 +0000 (02:36 +0000)]
Metavariable case in does_not_occur (hence weakly/stricly, positive, etc.)
relaxed. Is this always correct??

15 years agoMissing case for Match implemented.
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 02:35:28 +0000 (02:35 +0000)]
Missing case for Match implemented.

15 years ago...
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 02:24:37 +0000 (02:24 +0000)]
...

15 years agoweakly/strictly positive checks relaxed to allow metavariables that are not
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 02:23:02 +0000 (02:23 +0000)]
weakly/strictly positive checks relaxed to allow metavariables that are not
substituted

15 years ago...
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 02:13:35 +0000 (02:13 +0000)]
...

15 years agoImproved error message.
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 02:13:10 +0000 (02:13 +0000)]
Improved error message.

15 years agoBug fixed: the debrujinate function (hence the one to compute objects height)
Claudio Sacerdoti Coen [Wed, 8 Jul 2009 02:10:13 +0000 (02:10 +0000)]
Bug fixed: the debrujinate function (hence the one to compute objects height)
did not take the substitution.

15 years ago...
Claudio Sacerdoti Coen [Tue, 7 Jul 2009 22:10:33 +0000 (22:10 +0000)]
...

15 years agoBug fixed: one uri was not refreshed, causing divergence of the kernel!
Claudio Sacerdoti Coen [Tue, 7 Jul 2009 21:51:34 +0000 (21:51 +0000)]
Bug fixed: one uri was not refreshed, causing divergence of the kernel!

15 years agofixed some typos
Enrico Tassi [Tue, 7 Jul 2009 14:13:45 +0000 (14:13 +0000)]
fixed some typos

15 years agoLet's play a bit with NG.
Claudio Sacerdoti Coen [Tue, 7 Jul 2009 13:15:30 +0000 (13:15 +0000)]
Let's play a bit with NG.
This library is NOT meant to be the final one, just a way to experiment with
features.

15 years ago1) Include files for NG were neither recursively processes nor accumulated.
Claudio Sacerdoti Coen [Tue, 7 Jul 2009 01:49:29 +0000 (01:49 +0000)]
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)

15 years agoFixed printing of number of problems solved
denes [Mon, 6 Jul 2009 14:17:49 +0000 (14:17 +0000)]
Fixed printing of number of problems solved

15 years agoTried to implement lpo in a more efficient way
denes [Mon, 6 Jul 2009 10:28:04 +0000 (10:28 +0000)]
Tried to implement lpo in a more efficient way

15 years agoFixed typo in lpo (from old implementation)
denes [Mon, 6 Jul 2009 10:01:54 +0000 (10:01 +0000)]
Fixed typo in lpo (from old implementation)

15 years agosome corrections
Ferruccio Guidi [Fri, 3 Jul 2009 18:29:06 +0000 (18:29 +0000)]
some corrections

15 years agomore static analysis on the Automath text
Ferruccio Guidi [Fri, 3 Jul 2009 18:11:04 +0000 (18:11 +0000)]
more static analysis on the Automath text

15 years agoPorted old implementation of LPO (for test purposes)
denes [Fri, 3 Jul 2009 16:41:33 +0000 (16:41 +0000)]
Ported old implementation of LPO (for test purposes)

15 years agowe now do some static analysis on the Automath text to possibly clear some language...
Ferruccio Guidi [Fri, 3 Jul 2009 15:28:01 +0000 (15:28 +0000)]
we now do some static analysis on the Automath text to possibly clear some language ambiguities

15 years agoImplemented LPO
denes [Fri, 3 Jul 2009 13:22:28 +0000 (13:22 +0000)]
Implemented LPO

15 years agoCorrected type for bag
denes [Thu, 2 Jul 2009 14:29:01 +0000 (14:29 +0000)]
Corrected type for bag

15 years agoNew age selection
denes [Thu, 2 Jul 2009 14:20:38 +0000 (14:20 +0000)]
New age selection
New demodulation strategy

15 years agobetter output handling
Enrico Tassi [Thu, 2 Jul 2009 11:01:15 +0000 (11:01 +0000)]
better output handling

15 years agoreturn type of paramod fixed according to the SZSOntology
Enrico Tassi [Thu, 2 Jul 2009 10:57:00 +0000 (10:57 +0000)]
return type of paramod fixed according to the SZSOntology

15 years ago...
Enrico Tassi [Wed, 1 Jul 2009 16:13:33 +0000 (16:13 +0000)]
...

15 years ago...
Enrico Tassi [Wed, 1 Jul 2009 16:07:16 +0000 (16:07 +0000)]
...

15 years agoVersion number set to 1.0.0-rc1
Wilmer Ricciotti [Wed, 1 Jul 2009 13:56:38 +0000 (13:56 +0000)]
Version number set to 1.0.0-rc1

15 years agoFixed type of bag
denes [Wed, 1 Jul 2009 09:35:26 +0000 (09:35 +0000)]
Fixed type of bag

15 years agoparallel
Enrico Tassi [Tue, 30 Jun 2009 14:33:37 +0000 (14:33 +0000)]
parallel

15 years agoMoved ID management inside the bag
denes [Tue, 30 Jun 2009 14:12:52 +0000 (14:12 +0000)]
Moved ID management inside the bag

15 years agoattempt of using 2 different orderings
Enrico Tassi [Tue, 30 Jun 2009 13:07:35 +0000 (13:07 +0000)]
attempt of using 2 different orderings

15 years ago....
Enrico Tassi [Tue, 30 Jun 2009 12:35:21 +0000 (12:35 +0000)]
....

15 years agoCorrected a few typos
denes [Tue, 30 Jun 2009 12:07:20 +0000 (12:07 +0000)]
Corrected a few typos

15 years ago...
Enrico Tassi [Tue, 30 Jun 2009 11:54:21 +0000 (11:54 +0000)]
...

15 years agoEnabled age selection (ratio 1/5)
denes [Tue, 30 Jun 2009 10:20:40 +0000 (10:20 +0000)]
Enabled age selection (ratio 1/5)

15 years agolambda-delta:
Ferruccio Guidi [Mon, 29 Jun 2009 17:46:08 +0000 (17:46 +0000)]
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 :)

15 years ago...
Enrico Tassi [Mon, 29 Jun 2009 14:44:21 +0000 (14:44 +0000)]
...

15 years agodo not infer on closed goals
Enrico Tassi [Mon, 29 Jun 2009 14:36:37 +0000 (14:36 +0000)]
do not infer on closed goals

15 years agoremoved a maybe diverging test
Enrico Tassi [Mon, 29 Jun 2009 14:30:18 +0000 (14:30 +0000)]
removed a maybe diverging test

15 years ago...
Enrico Tassi [Mon, 29 Jun 2009 13:45:03 +0000 (13:45 +0000)]
...

15 years agoFirst attempt for refined goal selection strategy
denes [Mon, 29 Jun 2009 13:33:42 +0000 (13:33 +0000)]
First attempt for refined goal selection strategy

15 years agoadded (but not active) last chance idea
Enrico Tassi [Mon, 29 Jun 2009 12:59:20 +0000 (12:59 +0000)]
added (but not active) last chance idea

15 years agoImplemented orphan murdering technique
denes [Mon, 29 Jun 2009 10:41:50 +0000 (10:41 +0000)]
Implemented orphan murdering technique

15 years agonew make test target
Enrico Tassi [Mon, 29 Jun 2009 10:16:17 +0000 (10:16 +0000)]
new make test target

15 years agonew kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes
Ferruccio Guidi [Sun, 28 Jun 2009 17:59:13 +0000 (17:59 +0000)]
new kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes

15 years agoattempt to run a last chance procedure after the timeout
Andrea Asperti [Fri, 26 Jun 2009 15:38:56 +0000 (15:38 +0000)]
attempt to run a last chance procedure after the timeout

15 years agothe timeout is passed to test last chance
Andrea Asperti [Fri, 26 Jun 2009 15:38:02 +0000 (15:38 +0000)]
the timeout is passed to test last chance

15 years agothis case is not assert false since it can happen if occur_check
Andrea Asperti [Fri, 26 Jun 2009 13:47:25 +0000 (13:47 +0000)]
this case is not assert false since it can happen if occur_check
makes fail the unification

15 years agofixed parsing
Andrea Asperti [Fri, 26 Jun 2009 13:21:55 +0000 (13:21 +0000)]
fixed parsing

15 years agoconvenient problem lists
Andrea Asperti [Fri, 26 Jun 2009 12:01:30 +0000 (12:01 +0000)]
convenient problem lists

15 years agoan easy for loop
Andrea Asperti [Fri, 26 Jun 2009 12:01:01 +0000 (12:01 +0000)]
an easy for loop

15 years agodeep subsumption activated
Andrea Asperti [Fri, 26 Jun 2009 11:02:11 +0000 (11:02 +0000)]
deep subsumption activated

15 years agotest for deep subsumption added
Andrea Asperti [Fri, 26 Jun 2009 11:00:20 +0000 (11:00 +0000)]
test for deep subsumption added

15 years agoImplemented orphan murder test (clauses are not discarded for now)
denes [Fri, 26 Jun 2009 09:46:23 +0000 (09:46 +0000)]
Implemented orphan murder test (clauses are not discarded for now)
Re-enabled zero weight trick

15 years ago...
Enrico Tassi [Thu, 25 Jun 2009 21:29:22 +0000 (21:29 +0000)]
...

15 years agobetter doc
Enrico Tassi [Thu, 25 Jun 2009 21:23:44 +0000 (21:23 +0000)]
better doc

15 years agotimeouts are passed as arguments, so that tptpprover can
Enrico Tassi [Thu, 25 Jun 2009 20:54:52 +0000 (20:54 +0000)]
timeouts are passed as arguments, so that tptpprover can
accept --timeout argument. Moreover it prints the proof
according to the SZS ontology

15 years ago- some depend files :)
Ferruccio Guidi [Thu, 25 Jun 2009 19:16:36 +0000 (19:16 +0000)]
- some depend files :)

15 years agothe prover is almost OK, types in fuctors a bit extended to
Enrico Tassi [Thu, 25 Jun 2009 16:47:21 +0000 (16:47 +0000)]
the prover is almost OK, types in fuctors a bit extended to
ease their instantiation

15 years agoFirst version of deep_subsumption.
Andrea Asperti [Thu, 25 Jun 2009 15:55:14 +0000 (15:55 +0000)]
First version of deep_subsumption.

15 years agoVarious fixes
denes [Thu, 25 Jun 2009 15:24:09 +0000 (15:24 +0000)]
Various fixes

15 years agonew function
Enrico Tassi [Thu, 25 Jun 2009 15:10:43 +0000 (15:10 +0000)]
new function

15 years ago...
Enrico Tassi [Thu, 25 Jun 2009 14:45:37 +0000 (14:45 +0000)]
...

15 years agomatitaprover is almost there
Enrico Tassi [Thu, 25 Jun 2009 14:42:56 +0000 (14:42 +0000)]
matitaprover is almost there

15 years ago...
Enrico Tassi [Thu, 25 Jun 2009 13:12:52 +0000 (13:12 +0000)]
...

15 years agoinitial import of standalone matitaprover binary
Enrico Tassi [Thu, 25 Jun 2009 13:08:35 +0000 (13:08 +0000)]
initial import of standalone matitaprover binary

15 years agoNow using age selection
denes [Thu, 25 Jun 2009 12:19:45 +0000 (12:19 +0000)]
Now using age selection

15 years agocode refactoring for paramodulation
Enrico Tassi [Thu, 25 Jun 2009 10:17:36 +0000 (10:17 +0000)]
code refactoring for paramodulation

15 years agonew function list_mapi_acc
Enrico Tassi [Thu, 25 Jun 2009 10:17:13 +0000 (10:17 +0000)]
new function list_mapi_acc

15 years agoFixed is_identity for facts
denes [Thu, 25 Jun 2009 09:52:58 +0000 (09:52 +0000)]
Fixed is_identity for facts

15 years agoFixed insertion of passive clauses
denes [Thu, 25 Jun 2009 08:54:30 +0000 (08:54 +0000)]
Fixed insertion of passive clauses

15 years agoCode factorization
Andrea Asperti [Thu, 25 Jun 2009 08:53:38 +0000 (08:53 +0000)]
Code factorization

15 years agoRemoved debug printing
denes [Wed, 24 Jun 2009 17:02:25 +0000 (17:02 +0000)]
Removed debug printing

15 years agoNow inserting hypothesis and goal with zero weight
denes [Wed, 24 Jun 2009 16:59:41 +0000 (16:59 +0000)]
Now inserting hypothesis and goal with zero weight

15 years agoExtended is_identity test
denes [Wed, 24 Jun 2009 16:00:35 +0000 (16:00 +0000)]
Extended is_identity test
First step towards age selection

15 years agoImplemented check for duplicates (in goals)
denes [Wed, 24 Jun 2009 12:30:56 +0000 (12:30 +0000)]
Implemented check for duplicates (in goals)

15 years agoRemoved old debugging assertion
denes [Tue, 23 Jun 2009 22:46:49 +0000 (22:46 +0000)]
Removed old debugging assertion

15 years ago- procedural: basic support for lapply (solves a problem in the reconstruction of...
Ferruccio Guidi [Tue, 23 Jun 2009 21:00:06 +0000 (21:00 +0000)]
- procedural: basic support for lapply (solves a problem in the reconstruction of algebra/groups.ma)
- lambda-delta: bugfix in line counts and nodes counts

15 years agoRemoved debug printing raising Failure
denes [Tue, 23 Jun 2009 17:57:40 +0000 (17:57 +0000)]
Removed debug printing raising Failure

15 years agoRemoved debug printing
denes [Tue, 23 Jun 2009 17:10:40 +0000 (17:10 +0000)]
Removed debug printing

15 years agoRewrote the main loop for paramodulation
denes [Tue, 23 Jun 2009 16:56:02 +0000 (16:56 +0000)]
Rewrote the main loop for paramodulation

15 years agoundo/serialization for universes implemented
Enrico Tassi [Tue, 23 Jun 2009 16:00:55 +0000 (16:00 +0000)]
undo/serialization for universes implemented

15 years agoDebugging prerr_endlines removed.
Claudio Sacerdoti Coen [Tue, 23 Jun 2009 11:46:42 +0000 (11:46 +0000)]
Debugging prerr_endlines removed.

15 years ago1) NCicTypechecker.typecheck_obj removed, since it did not add to the
Claudio Sacerdoti Coen [Tue, 23 Jun 2009 11:46:16 +0000 (11:46 +0000)]
1) NCicTypechecker.typecheck_obj removed, since it did not add to the
   environment (and thus all objects were type-checked at least twice)
2) NCicEnvironment.check_and_add_obj that checks and add an object
3) added NCicEnvironment.invalidate_obj that invalidate all objects after a
   given one (that comprised)
4) NCicLibrary.add_obj now calls the NCicEnvironment.check_and_add_obj;
   NCicLibrary.time_travel now calls NCicEnvironment.invalidate_obj

Note: it could happen that an object is in the environment but not in the
      library and thus it could not be invalidated by time_travel.
      In practice, this is safe anyway and it will never happen.

15 years agoFixed nasty bug in maxvar updating
denes [Tue, 23 Jun 2009 10:30:55 +0000 (10:30 +0000)]
Fixed nasty bug in maxvar updating

15 years ago- Bug fixed: removed URIs were not removed from the dependencies DB.
Claudio Sacerdoti Coen [Tue, 23 Jun 2009 10:23:59 +0000 (10:23 +0000)]
- Bug fixed: removed URIs were not removed from the dependencies DB.
- The assert failure has been removed since in some situations (????) an
  empty dir (no new objects) was not created and thus it was normal that it
  was not removed. TO BE BETTER UNDERSTOOD

15 years agoremoved problem not in UEQ
Enrico Tassi [Tue, 23 Jun 2009 08:07:22 +0000 (08:07 +0000)]
removed problem not in UEQ

15 years ago- nodes count is now working for aut and meta
Ferruccio Guidi [Mon, 22 Jun 2009 22:53:12 +0000 (22:53 +0000)]
- nodes count is now working for aut and meta
- bugfix in autLexer
- comment fix in aut

15 years agoAdded more precise time information
denes [Mon, 22 Jun 2009 17:12:49 +0000 (17:12 +0000)]
Added more precise time information

15 years agoAdded problems from CASC 208
denes [Mon, 22 Jun 2009 17:03:32 +0000 (17:03 +0000)]
Added problems from CASC 208

15 years agoRegenerated problems with corrected tptp2grafite
denes [Mon, 22 Jun 2009 16:58:17 +0000 (16:58 +0000)]
Regenerated problems with corrected tptp2grafite

15 years agoCorrected proof visiting (topological sort)
denes [Mon, 22 Jun 2009 16:51:14 +0000 (16:51 +0000)]
Corrected proof visiting (topological sort)

15 years agoSmall debugging in tptp2grafite
denes [Mon, 22 Jun 2009 16:50:37 +0000 (16:50 +0000)]
Small debugging in tptp2grafite

15 years agoAdded injective compose
Wilmer Ricciotti [Sun, 21 Jun 2009 18:32:22 +0000 (18:32 +0000)]
Added injective compose