| 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 |
| 2009-05-05 |
Enrico Tassi | - pretty printer made robust in face of list_nth
|
commit | commitdiff | tree |
| 2009-05-05 |
Enrico Tassi | more tests
|
commit | commitdiff | tree |
| 2009-04-30 |
Enrico Tassi | run check_if_goal_is_solved on all goals (active+passive)
|
commit | commitdiff | tree |
| 2009-04-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-04-29 |
Enrico Tassi | call paramod instead of solve_Rewrite
|
commit | commitdiff | tree |
| 2009-04-29 |
Enrico Tassi | no typing
|
commit | commitdiff | tree |
| 2009-04-29 |
Enrico Tassi | many checks guarded with if Utils.debug_metas
|
commit | commitdiff | tree |
| 2009-04-28 |
Enrico Tassi | depenalization of smart apply inside auto, that is...
|
commit | commitdiff | tree |
| 2009-04-28 |
Enrico Tassi | fixed bug, demodulation was keeping results not strictly...
|
commit | commitdiff | tree |
| 2009-04-28 |
Enrico Tassi | huge commit in automation:
|
commit | commitdiff | tree |
| 2009-04-22 |
Enrico Tassi | demodulate takes an extra argument 'all', if present...
|
commit | commitdiff | tree |
| 2009-04-21 |
Enrico Tassi | fixed last file restricting auto tables
|
commit | commitdiff | tree |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_cache
|
commit | commitdiff | tree |
| 2009-04-16 |
Enrico Tassi | Universe is used only locally to tactics/
|
commit | commitdiff | tree |
| 2009-04-16 |
Enrico Tassi | added an exception
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | added letin, still broken
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | new tactic whd implemented
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | - change implemented in 4 lines
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | - generalize finished
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | ?_OS1 := C[ ?_IN ]
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | fixed modules order
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | minor fixes
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-04-08 |
Enrico Tassi | generalized is half-implemented (still broken)
|
commit | commitdiff | tree |
| 2009-04-08 |
Enrico Tassi | Analizyng the inductive type of the eliminated term and
|
commit | commitdiff | tree |
| 2009-04-07 |
Enrico Tassi | - select_tac honors the hypotheses pattern when required...
|
commit | commitdiff | tree |
| 2009-04-07 |
Enrico Tassi | select honors the substitution
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | tactic cases works! delift clears tags
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | eta-contraction was made on the wrong term
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | unification:
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | better error message
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | added one exception
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2009-04-02 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-04-02 |
Enrico Tassi | New file nTacStatus to:
|
commit | commitdiff | tree |
| next |
projects / helm.git / search