| 2009-07-13 |
Enrico Tassi | matitaprover is now flexible enough to allow the computation...
|
commit | commitdiff | tree |
| 2009-07-10 |
Enrico Tassi | initial implementation of coercion composition
|
commit | commitdiff | tree |
| 2009-07-10 |
Enrico Tassi | more work on coercions composition
|
commit | commitdiff | tree |
| 2009-07-10 |
Enrico Tassi | more profilers
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | claudio, please have a look at this
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | new nrepeat (and block '('...')' ) tactical
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | New functorialization: paramod is abstracted over a...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | profile most operations, do not return a filtered varlist...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | 1 process for now
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | two cases should be assert false at least in TPTP
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | micro optimizations to unification
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | activate kbo, not lpo
|
commit | commitdiff | tree |
| 2009-07-08 |
Enrico Tassi | few more files, one diverges
|
commit | commitdiff | tree |
| 2009-07-08 |
Enrico Tassi | removed useless universes
|
commit | commitdiff | tree |
| 2009-07-08 |
Enrico Tassi | import of a sample for cosimo
|
commit | commitdiff | tree |
| 2009-07-07 |
Enrico Tassi | fixed some typos
|
commit | commitdiff | tree |
| 2009-07-02 |
Enrico Tassi | better output handling
|
commit | commitdiff | tree |
| 2009-07-02 |
Enrico Tassi | return type of paramod fixed according to the SZSOntology
|
commit | commitdiff | tree |
| 2009-07-01 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-07-01 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-30 |
Enrico Tassi | parallel
|
commit | commitdiff | tree |
| 2009-06-30 |
Enrico Tassi | attempt of using 2 different orderings
|
commit | commitdiff | tree |
| 2009-06-30 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2009-06-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | do not infer on closed goals
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | removed a maybe diverging test
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | added (but not active) last chance idea
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | new make test target
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | better doc
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | timeouts are passed as arguments, so that tptpprover can
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | the prover is almost OK, types in fuctors a bit extended to
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | new function
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | matitaprover is almost there
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | initial import of standalone matitaprover binary
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | code refactoring for paramodulation
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | new function list_mapi_acc
|
commit | commitdiff | tree |
| 2009-06-23 |
Enrico Tassi | undo/serialization for universes implemented
|
commit | commitdiff | tree |
| 2009-06-23 |
Enrico Tassi | removed problem not in UEQ
|
commit | commitdiff | tree |
| 2009-06-18 |
Enrico Tassi | debug pps removed
|
commit | commitdiff | tree |
| 2009-06-18 |
Enrico Tassi | better exception handling
|
commit | commitdiff | tree |
| 2009-06-18 |
Enrico Tassi | proof patching!
|
commit | commitdiff | tree |
| 2009-06-18 |
Enrico Tassi | callbacks were taking in input a status bu were not...
|
commit | commitdiff | tree |
| 2009-06-17 |
Enrico Tassi | proof reconstruction almost OK
|
commit | commitdiff | tree |
| 2009-06-16 |
Enrico Tassi | first proof reconstruction attempt, still bugged since it
|
commit | commitdiff | tree |
| 2009-06-16 |
Enrico Tassi | avoid fixing non-recursive terms
|
commit | commitdiff | tree |
| 2009-06-16 |
Enrico Tassi | we fix recursive object reference with the correct...
|
commit | commitdiff | tree |
| 2009-06-15 |
Enrico Tassi | EXPERIMENTAL COMMIT (part B, by CSC :-):
|
commit | commitdiff | tree |
| 2009-06-15 |
Enrico Tassi | EXPERIMENTAL COMMIT (by CSC,actuall :-)
|
commit | commitdiff | tree |
| 2009-06-15 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-15 |
Enrico Tassi | added TODO list
|
commit | commitdiff | tree |
| 2009-06-15 |
Enrico Tassi | huge commit regarding the grafite_status:
|
commit | commitdiff | tree |
| 2009-06-15 |
Enrico Tassi | part of last commit
|
commit | commitdiff | tree |
| 2009-06-15 |
Enrico Tassi | tacticals are really tactics now, they have an AST...
|
commit | commitdiff | tree |
| 2009-06-12 |
Enrico Tassi | -ng implemented
|
commit | commitdiff | tree |
| 2009-06-11 |
Enrico Tassi | content2pres for the new cic fixed
|
commit | commitdiff | tree |
| 2009-06-10 |
Enrico Tassi | 1) added simplification of actives w.r.t. selected
|
commit | commitdiff | tree |
| 2009-06-10 |
Enrico Tassi | right inference step completed
|
commit | commitdiff | tree |
| 2009-06-10 |
Enrico Tassi | new function filter_map_acc
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | almost complete superposition right step
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | see the previous commit
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | termAcicContent is logic independent (despite its name...
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | snaphost: supright almost done
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | fixed metas
|
commit | commitdiff | tree |
| 2009-06-09 |
Enrico Tassi | fixed building
|
commit | commitdiff | tree |
| 2009-06-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-08 |
Enrico Tassi | a skeleton of supright
|
commit | commitdiff | tree |
| 2009-06-08 |
Enrico Tassi | some more functors and a nice higher-order all_positions...
|
commit | commitdiff | tree |
| 2009-06-08 |
Enrico Tassi | added META for ng_paramodulation
|
commit | commitdiff | tree |
| 2009-06-06 |
Enrico Tassi | some renaming to make ocamlopt happy
|
commit | commitdiff | tree |
| 2009-06-04 |
Enrico Tassi | minor changes here and there. We extend fo-unification...
|
commit | commitdiff | tree |
| 2009-06-04 |
Enrico Tassi | comments
|
commit | commitdiff | tree |
| 2009-06-04 |
Enrico Tassi | better type for comparison and implementation of KBO...
|
commit | commitdiff | tree |
| 2009-06-04 |
Enrico Tassi | more functors
|
commit | commitdiff | tree |
| 2009-06-03 |
Enrico Tassi | functorial abstraction over term blobs
|
commit | commitdiff | tree |
| 2009-06-01 |
Enrico Tassi | added a snapshot of comparison
|
commit | commitdiff | tree |
| 2009-06-01 |
Enrico Tassi | we rewrite the paramodulation code!
|
commit | commitdiff | tree |
| 2009-05-25 |
Enrico Tassi | nasty change in the lexer/parser:
|
commit | commitdiff | tree |
| 2009-05-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-05-19 |
Enrico Tassi | regenerated
|
commit | commitdiff | tree |
| 2009-05-19 |
Enrico Tassi | fixed generation of horn clauses, negated atoms are...
|
commit | commitdiff | tree |
| 2009-05-19 |
Enrico Tassi | some horn+equality problems
|
commit | commitdiff | tree |
| 2009-05-18 |
Enrico Tassi | removed useless function
|
commit | commitdiff | tree |
| 2009-05-18 |
Enrico Tassi | in the new kernel you can type Type[i] to mean Type_i...
|
commit | commitdiff | tree |
| 2009-05-18 |
Enrico Tassi | nothing special
|
commit | commitdiff | tree |
| 2009-05-17 |
Enrico Tassi | byte tests disabled
|
commit | commitdiff | tree |
| 2009-05-15 |
Enrico Tassi | added patch to not unify any term containing the in_scope...
|
commit | commitdiff | tree |
| 2009-05-06 |
Enrico Tassi | apply and auto.equational_case call saturation.solve_narrowing
|
commit | commitdiff | tree |
| 2009-05-06 |
Enrico Tassi | updated comment
|
commit | commitdiff | tree |
| next |
projects / helm.git / search