]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2009-09-25 denesPorted innermost strategy for demodulation from trunk
2009-07-31 denesFixed (yet another) nasty bug, in deep_eq this time
2009-07-31 denesFixed nasty bug in superposition and freshing of clauses
2009-07-31 denesNow iterating superposition
2009-07-30 denesPorted demodulation on clauses
2009-07-30 denesAdded check for trivial (identity) goal
2009-07-29 denesUpdate eligible problem list (now sorted)
2009-07-29 denesAdded TreeLimitRun
2009-07-29 denesAdded Clauses module
2009-07-29 denesAdded symbolic link to clauses
2009-07-29 denesReorganized foUtils, added Clauses module to avoid...
2009-07-28 denesVarious architectural changes
2009-07-28 denesVarious architectural changes
2009-07-24 denesAdded symbolic links to hTopoSort
2009-07-24 denesFixed pretty printer and debug printings
2009-07-23 denesFirst compiling version
2009-07-23 denesFixed useage
2009-07-22 denesFixes
2009-07-22 denesFixed conflicts due to problem when merging with UEQ...
2009-07-17 denesBranched paramodulation for CNF (Horn clauses)
2009-07-15 Enrico Tassincopy partially implemented and fixed (a ?) chain to...
2009-07-15 Wilmer RicciottiFixed dependency function, which was lacking the code...
2009-07-15 Enrico Tassi...
2009-07-15 Enrico Tassimatch_coercion gives back the saturations, not the...
2009-07-15 Cosimo Oliboni freescale porting, work in progress
2009-07-14 denesFixed Option type error (OCaml bug)
2009-07-14 denes.
2009-07-14 denes.
2009-07-14 Cosimo Oliboni freescale porting to ng, work in progress
2009-07-13 Enrico Tassibetter spacing
2009-07-13 Enrico Tassistatistics are used, when possible, to sort
2009-07-13 denesAdded statistics printings
2009-07-13 denesAdded statistics module
2009-07-13 Claudio Sacerdoti... First proof finished (some tactics still not working).
2009-07-13 Enrico Tassimatitaprover is now flexible enough to allow the comput...
2009-07-13 Claudio Sacerdoti... Coercion hiding implemented. Notes:
2009-07-13 Cosimo Oliboni freescale translation (work in progress)
2009-07-12 Cosimo Oliboni(no commit message)
2009-07-11 Cosimo Oliboni(no commit message)
2009-07-10 Claudio Sacerdoti... Composite coercions are here!
2009-07-10 Ferruccio Guidi- brgOutput: the nodes count is now implemented
2009-07-10 Enrico Tassiinitial implementation of coercion composition
2009-07-10 Enrico Tassimore work on coercions composition
2009-07-10 Cosimo Oliboni +root +depends
2009-07-10 denesRemoved unused parameter of unification procedure ...
2009-07-10 Enrico Tassimore profilers
2009-07-10 Claudio Sacerdoti... Coercions used here and there.
2009-07-10 Claudio Sacerdoti... Bug fixed (missing ctx) + comment added.
2009-07-10 Claudio Sacerdoti... ...
2009-07-10 Cosimo Oliboninew ng freescale, no external dependencies
2009-07-10 Claudio Sacerdoti... Let's live with new ocaml type system limitations...
2009-07-09 Enrico Tassiinitial implementation of `ncoercion name : type :...
2009-07-09 Enrico Tassiclaudio, please have a look at this
2009-07-09 Enrico Tassinew nrepeat (and block '('...')' ) tactical
2009-07-09 Enrico Tassi...
2009-07-09 Enrico TassiNew functorialization: paramod is abstracted over a...
2009-07-09 denesFixed check for condition iv p.33 (Riazzanov)
2009-07-09 Wilmer RicciottiMore updates to Fsub.
2009-07-09 Enrico Tassiprofile most operations, do not return a filtered varli...
2009-07-09 Enrico Tassi1 process for now
2009-07-09 Enrico Tassitwo cases should be assert false at least in TPTP
2009-07-09 Enrico Tassimicro optimizations to unification
2009-07-09 denesCleaned a bit
2009-07-09 Enrico Tassi...
2009-07-09 Enrico Tassiactivate kbo, not lpo
2009-07-09 Claudio Sacerdoti... ...
2009-07-09 Claudio Sacerdoti... Bug fixed (non-captured variable).
2009-07-08 Claudio Sacerdoti... eq moved to CProp
2009-07-08 Claudio Sacerdoti... ...
2009-07-08 Claudio Sacerdoti... repeat_tac
2009-07-08 Claudio Sacerdoti... ...
2009-07-08 Enrico Tassifew more files, one diverges
2009-07-08 Cosimo Olibonidirectory for porting the assembly to matita-ng
2009-07-08 Enrico Tassiremoved useless universes
2009-07-08 Enrico Tassiimport of a sample for cosimo
2009-07-08 Claudio Sacerdoti... Hmmmm. This way we need "canonical structures" also...
2009-07-08 Claudio Sacerdoti... ...
2009-07-08 Claudio Sacerdoti... Metavariable case in does_not_occur (hence weakly/stric...
2009-07-08 Claudio Sacerdoti... Missing case for Match implemented.
2009-07-08 Claudio Sacerdoti... ...
2009-07-08 Claudio Sacerdoti... weakly/strictly positive checks relaxed to allow metava...
2009-07-08 Claudio Sacerdoti... ...
2009-07-08 Claudio Sacerdoti... Improved error message.
2009-07-08 Claudio Sacerdoti... Bug fixed: the debrujinate function (hence the one...
2009-07-07 Claudio Sacerdoti... ...
2009-07-07 Claudio Sacerdoti... Bug fixed: one uri was not refreshed, causing divergenc...
2009-07-07 Enrico Tassifixed some typos
2009-07-07 Claudio Sacerdoti... Let's play a bit with NG.
2009-07-07 Claudio Sacerdoti... 1) Include files for NG were neither recursively proces...
2009-07-06 denesFixed printing of number of problems solved
2009-07-06 denesTried to implement lpo in a more efficient way
2009-07-06 denesFixed typo in lpo (from old implementation)
2009-07-03 Ferruccio Guidisome corrections
2009-07-03 Ferruccio Guidimore static analysis on the Automath text
2009-07-03 denesPorted old implementation of LPO (for test purposes)
2009-07-03 Ferruccio Guidiwe now do some static analysis on the Automath text...
2009-07-03 denesImplemented LPO
2009-07-02 denesCorrected type for bag
2009-07-02 denesNew age selection
2009-07-02 Enrico Tassibetter output handling
next