| 2006-07-27 |
Claudio Sacerdoti... | More debugging output on stderr. |
tree | commitdiff |
| 2006-07-27 |
maiorino | Automation enabled for declarative proofs. Cool. |
tree | commitdiff |
| 2006-07-27 |
maiorino | "that is equivalent to" and "or equivalently" implement... |
tree | commitdiff |
| 2006-07-27 |
maiorino | All the declarative tactics now have a more or less... |
tree | commitdiff |
| 2006-07-27 |
maiorino | Declarative tactics for rewriting steps, elimination... |
tree | commitdiff |
| 2006-07-27 |
maiorino | New declarative commands (ast, pretty-printing and... |
tree | commitdiff |
| 2006-07-27 |
Claudio Sacerdoti... | print_endline => prerr_endline |
tree | commitdiff |
| 2006-07-26 |
Claudio Sacerdoti... | Elim now performs whd to find the inductive type. |
tree | commitdiff |
| 2006-07-26 |
Enrico Tassi | order is important |
tree | commitdiff |
| 2006-07-24 |
Enrico Tassi | added timeout parameter to auto paramodulation. |
tree | commitdiff |
| 2006-07-24 |
Enrico Tassi | more work on matitaprover (no more XML and buris are... |
tree | commitdiff |
| 2006-07-23 |
Enrico Tassi | see BOO025-1 as an example of failure if (mot p) is... |
tree | commitdiff |
| 2006-07-22 |
Enrico Tassi | matitaprover |
tree | commitdiff |
| 2006-07-20 |
Enrico Tassi | trans chains even inside letins body |
tree | commitdiff |
| 2006-07-20 |
Enrico Tassi | removed abstractios for dummy metavariables when genera... |
tree | commitdiff |
| 2006-07-19 |
Claudio Sacerdoti... | Bug fixed in rewrite in multiple hypothesis and/or... |
tree | commitdiff |
| 2006-07-19 |
Claudio Sacerdoti... | Serious bug fixed in simplify: sometimes terms wwere... |
tree | commitdiff |
| 2006-07-14 |
Andrea Asperti | Added the computation of max_weight for equations in... |
tree | commitdiff |
| 2006-07-12 |
Claudio Sacerdoti... | Missing copyright added to tactics/declarative.ml* |
tree | commitdiff |
| 2006-07-11 |
maiorino | First experimental version of the declarative proof... |
tree | commitdiff |
| 2006-07-11 |
Enrico Tassi | - removed Positive and Negative (all is positive) |
tree | commitdiff |
| 2006-07-10 |
Enrico Tassi | fixed 1,2: and *: according to the camera ready semantics |
tree | commitdiff |
| 2006-07-06 |
Enrico Tassi | fixed *: and n,m: |
tree | commitdiff |
| 2006-07-03 |
Enrico Tassi | - patch to consider the symbols of the goal when comput... |
tree | commitdiff |
| 2006-06-30 |
Enrico Tassi | pretty proofs are back |
tree | commitdiff |
| 2006-06-29 |
Andrea Asperti | Cleaning up; removed a couple of "open". |
tree | commitdiff |
| 2006-06-29 |
Claudio Sacerdoti... | Demodulate used to be a reduction_kind and it used... |
tree | commitdiff |
| 2006-06-29 |
Claudio Sacerdoti... | WORK IN PROGRESS: |
tree | commitdiff |
| 2006-06-29 |
Enrico Tassi | before goals are inferred with current, |
tree | commitdiff |
| 2006-06-29 |
Enrico Tassi | goals after a superposition step are relocated |
tree | commitdiff |
| 2006-06-28 |
Ferruccio Guidi | - "linear" flag added to lapply (automatic clearing) |
tree | commitdiff |
| 2006-06-28 |
Enrico Tassi | karma: every term the rewrite acts on must be substututed |
tree | commitdiff |
| 2006-06-28 |
Enrico Tassi | superposition_left not performed if the input goal... |
tree | commitdiff |
| 2006-06-27 |
Ferruccio Guidi | - decompose now runs with no arguments (operates on... |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | fixed infer_goal, added simplification before inferring... |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | using the new metadataConstraint function |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | used the new metadataConstraint function to retrieve... |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | fixed equalities_for_goal |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | the old compute_eq_weight is back (no more max) |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | fixed generation of letins |
tree | commitdiff |
| 2006-06-26 |
Enrico Tassi | more work for the generic auto parameters |
tree | commitdiff |
| 2006-06-21 |
Enrico Tassi | added the geniric |
tree | commitdiff |
| 2006-06-20 |
Enrico Tassi | garbage collection of dead equalities implemented |
tree | commitdiff |
| 2006-06-19 |
Enrico Tassi | typo cpying the formal semantic |
tree | commitdiff |
| 2006-06-19 |
Enrico Tassi | reorganized guiven_clause to work with the on_the_fly... |
tree | commitdiff |
| 2006-06-19 |
Enrico Tassi | demodulation of goal activated again. |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | some experiments |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | added (but still unused) remove_local_context |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | added (but not yet used) remove_local_context |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | Utils.compare_terms instead of compare_weights |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | occur_check and unification fixed. now Meta(i,[]) and... |
tree | commitdiff |
| 2006-06-18 |
Enrico Tassi | - some fixes regarding URIs of equality that now should... |
tree | commitdiff |
| 2006-06-15 |
Andrea Asperti | added applyS |
tree | commitdiff |
| 2006-06-15 |
Andrea Asperti | some fixed done in Orsay: |
tree | commitdiff |
| 2006-06-15 |
Andrea Asperti | exported 2 functions needed by applyS |
tree | commitdiff |
| 2006-06-15 |
Andrea Asperti | ... |
tree | commitdiff |
| 2006-06-11 |
Ferruccio Guidi | - slight fix in lapply syntax |
tree | commitdiff |
| 2006-06-09 |
Claudio Sacerdoti... | 1. the default for the default equality/absurd/true... |
tree | commitdiff |
| 2006-06-01 |
Stefano Zacchiroli | implemented tinycals: |
tree | commitdiff |
| 2006-06-01 |
Enrico Tassi | fix |
tree | commitdiff |
| 2006-06-01 |
Andrea Asperti | Subsumption_subst must be applied to the initial proof... |
tree | commitdiff |
| 2006-05-31 |
Enrico Tassi | fixed proofs, contextualization should now work. |
tree | commitdiff |
| 2006-05-30 |
Enrico Tassi | letin are now sorted properly. |
tree | commitdiff |
| 2006-05-30 |
Enrico Tassi | fixed proof generation again |
tree | commitdiff |
| 2006-05-30 |
Enrico Tassi | canonical and contextualize_rewrites are back, they... |
tree | commitdiff |
| 2006-05-30 |
Enrico Tassi | the function to create on the fly a symmetry step has... |
tree | commitdiff |
| 2006-05-29 |
Enrico Tassi | profilings are printed |
tree | commitdiff |
| 2006-05-29 |
Enrico Tassi | - proofs by subsumption now add a symmetry step if... |
tree | commitdiff |
| 2006-05-28 |
Enrico Tassi | weak equality on meta used when replacing. |
tree | commitdiff |
| 2006-05-28 |
Enrico Tassi | added the rule field to goal_proof. |
tree | commitdiff |
| 2006-05-28 |
Enrico Tassi | - fixed a bug in unification (not sure in the right... |
tree | commitdiff |
| 2006-05-26 |
Andrea Asperti | 1) variables occurring only in proofs anre not relocated |
tree | commitdiff |
| 2006-05-23 |
Andrea Asperti | added important comment |
tree | commitdiff |
| 2006-05-23 |
Andrea Asperti | fixed LetIn proofs |
tree | commitdiff |
| 2006-05-23 |
Enrico Tassi | added again stuff for profiling |
tree | commitdiff |
| 2006-05-23 |
Andrea Asperti | added stuff for profiling macros |
tree | commitdiff |
| 2006-05-22 |
Enrico Tassi | - code cleanup, especialli in Indexing where all the... |
tree | commitdiff |
| 2006-05-20 |
Enrico Tassi | removed prerr_endline. |
tree | commitdiff |
| 2006-05-20 |
Enrico Tassi | commented out a line to help paramodulation. |
tree | commitdiff |
| 2006-05-20 |
Enrico Tassi | fixed wrong calculation of free_metas |
tree | commitdiff |
| 2006-05-20 |
Enrico Tassi | removed a bad prerr_endline |
tree | commitdiff |
| 2006-05-20 |
Enrico Tassi | removed prerr_endline |
tree | commitdiff |
| 2006-05-20 |
Enrico Tassi | removedx a prerr_endline |
tree | commitdiff |
| 2006-05-20 |
Enrico Tassi | fixed demodulation of goal |
tree | commitdiff |
| 2006-05-19 |
Enrico Tassi | - metas_of_term moved to cicUtil |
tree | commitdiff |
| 2006-05-18 |
Enrico Tassi | existential variables in goal supported |
tree | commitdiff |
| 2006-05-16 |
Enrico Tassi | fixed subsumption_aux |
tree | commitdiff |
| 2006-05-16 |
Enrico Tassi | utf8_macros moved to syntax_extensions. |
tree | commitdiff |
| 2006-05-15 |
Enrico Tassi | - new given_clause |
tree | commitdiff |
| 2006-05-14 |
Enrico Tassi | - Removed old proofs |
tree | commitdiff |
| 2006-05-05 |
Andrea Asperti | New version of deep_subsumption |
tree | commitdiff |
| 2006-05-04 |
Enrico Tassi | goal demodulated with new |
tree | commitdiff |
| 2006-05-04 |
Enrico Tassi | new pp function for proofs |
tree | commitdiff |
| 2006-05-03 |
Enrico Tassi | more transitivity on proofs |
tree | commitdiff |
| 2006-04-26 |
Andrea Asperti | Build_proof_goal does not return the metasenv any more. |
tree | commitdiff |
| 2006-04-26 |
Andrea Asperti | fixed demodulation_goal (used to return always false) |
tree | commitdiff |
| 2006-04-26 |
Andrea Asperti | removed ocaml equality on equations |
tree | commitdiff |
| 2006-04-26 |
Enrico Tassi | more cleanup |
tree | commitdiff |
| 2006-04-26 |
Enrico Tassi | cleanup of saturate |
tree | commitdiff |
| 2006-04-26 |
Enrico Tassi | added a new type for proofs. |
tree | commitdiff |
| next |
projects / helm.git / history