2009-07-20 |
Claudio Sacerdoti... | Very serious bug fixed in unification, but the fix... |
tree | commitdiff |
2009-07-20 |
Claudio Sacerdoti... | 1) The NG kernel now accepts only usage of declared... |
tree | commitdiff |
2009-07-20 |
denes | One-side indexing for commutativity |
tree | commitdiff |
2009-07-20 |
denes | No demod call on functionnal symbols |
tree | commitdiff |
2009-07-20 |
Claudio Sacerdoti... | 1) ppmetasenv and ppcontext to reduce the amount of... |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | nelim now uses the appropriate _rect_XXX elimination... |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | 1) the user is notified when a new object is defined |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | More info to refine empty types elimination. |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | Generation of principles is now atomic. |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | Debugging code commented out. |
tree | commitdiff |
2009-07-17 |
Enrico Tassi | add comment |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | Bug fixed: singleton application. |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | New suffixes for elimination principles: |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | 1) added a function to retrieve all the universes curre... |
tree | commitdiff |
2009-07-17 |
Claudio Sacerdoti... | Generation of inductive principle for Type[0]. |
tree | commitdiff |
2009-07-16 |
denes | Sorted version of eligible problems list |
tree | commitdiff |
2009-07-16 |
denes | Disabled age selection and ad hoc goal weight computation |
tree | commitdiff |
2009-07-15 |
Enrico Tassi | ncopy partially implemented and fixed (a ?) chain to... |
tree | commitdiff |
2009-07-15 |
Wilmer Ricciotti | Fixed dependency function, which was lacking the code... |
tree | commitdiff |
2009-07-15 |
Enrico Tassi | ... |
tree | commitdiff |
2009-07-15 |
Enrico Tassi | match_coercion gives back the saturations, not the... |
tree | commitdiff |
2009-07-14 |
denes | Fixed Option type error (OCaml bug) |
tree | commitdiff |
2009-07-14 |
denes | . |
tree | commitdiff |
2009-07-14 |
denes | . |
tree | commitdiff |
2009-07-13 |
Enrico Tassi | better spacing |
tree | commitdiff |
2009-07-13 |
Enrico Tassi | statistics are used, when possible, to sort |
tree | commitdiff |
2009-07-13 |
denes | Added statistics printings |
tree | commitdiff |
2009-07-13 |
denes | Added statistics module |
tree | commitdiff |
2009-07-13 |
Enrico Tassi | matitaprover is now flexible enough to allow the comput... |
tree | commitdiff |
2009-07-13 |
Claudio Sacerdoti... | Coercion hiding implemented. Notes: |
tree | commitdiff |
2009-07-10 |
Enrico Tassi | initial implementation of coercion composition |
tree | commitdiff |
2009-07-10 |
denes | Removed unused parameter of unification procedure ... |
tree | commitdiff |
2009-07-10 |
Enrico Tassi | more profilers |
tree | commitdiff |
2009-07-10 |
Claudio Sacerdoti... | Bug fixed (missing ctx) + comment added. |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :... |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | new nrepeat (and block '('...')' ) tactical |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | New functorialization: paramod is abstracted over a... |
tree | commitdiff |
2009-07-09 |
denes | Fixed check for condition iv p.33 (Riazzanov) |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | profile most operations, do not return a filtered varli... |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | 1 process for now |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | two cases should be assert false at least in TPTP |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | micro optimizations to unification |
tree | commitdiff |
2009-07-09 |
denes | Cleaned a bit |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | ... |
tree | commitdiff |
2009-07-09 |
Enrico Tassi | activate kbo, not lpo |
tree | commitdiff |
2009-07-09 |
Claudio Sacerdoti... | Bug fixed (non-captured variable). |
tree | commitdiff |
2009-07-08 |
Claudio Sacerdoti... | repeat_tac |
tree | commitdiff |
2009-07-08 |
Claudio Sacerdoti... | Metavariable case in does_not_occur (hence weakly/stric... |
tree | commitdiff |
2009-07-08 |
Claudio Sacerdoti... | Missing case for Match implemented. |
tree | commitdiff |
2009-07-08 |
Claudio Sacerdoti... | weakly/strictly positive checks relaxed to allow metava... |
tree | commitdiff |
2009-07-08 |
Claudio Sacerdoti... | Improved error message. |
tree | commitdiff |
2009-07-08 |
Claudio Sacerdoti... | Bug fixed: the debrujinate function (hence the one... |
tree | commitdiff |
2009-07-07 |
Claudio Sacerdoti... | Bug fixed: one uri was not refreshed, causing divergenc... |
tree | commitdiff |
2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
tree | commitdiff |
2009-07-06 |
denes | Fixed printing of number of problems solved |
tree | commitdiff |
2009-07-06 |
denes | Tried to implement lpo in a more efficient way |
tree | commitdiff |
2009-07-06 |
denes | Fixed typo in lpo (from old implementation) |
tree | commitdiff |
2009-07-03 |
denes | Ported old implementation of LPO (for test purposes) |
tree | commitdiff |
2009-07-03 |
denes | Implemented LPO |
tree | commitdiff |
2009-07-02 |
denes | Corrected type for bag |
tree | commitdiff |
2009-07-02 |
denes | New age selection |
tree | commitdiff |
2009-07-02 |
Enrico Tassi | better output handling |
tree | commitdiff |
2009-07-02 |
Enrico Tassi | return type of paramod fixed according to the SZSOntology |
tree | commitdiff |
2009-07-01 |
Enrico Tassi | ... |
tree | commitdiff |
2009-07-01 |
Enrico Tassi | ... |
tree | commitdiff |
2009-07-01 |
Wilmer Ricciotti | Version number set to 1.0.0-rc1 |
tree | commitdiff |
2009-07-01 |
denes | Fixed type of bag |
tree | commitdiff |
2009-06-30 |
Enrico Tassi | parallel |
tree | commitdiff |
2009-06-30 |
denes | Moved ID management inside the bag |
tree | commitdiff |
2009-06-30 |
Enrico Tassi | attempt of using 2 different orderings |
tree | commitdiff |
2009-06-30 |
Enrico Tassi | .... |
tree | commitdiff |
2009-06-30 |
denes | Corrected a few typos |
tree | commitdiff |
2009-06-30 |
Enrico Tassi | ... |
tree | commitdiff |
2009-06-30 |
denes | Enabled age selection (ratio 1/5) |
tree | commitdiff |
2009-06-29 |
Enrico Tassi | ... |
tree | commitdiff |
2009-06-29 |
Enrico Tassi | do not infer on closed goals |
tree | commitdiff |
2009-06-29 |
Enrico Tassi | ... |
tree | commitdiff |
2009-06-29 |
denes | First attempt for refined goal selection strategy |
tree | commitdiff |
2009-06-29 |
Enrico Tassi | added (but not active) last chance idea |
tree | commitdiff |
2009-06-29 |
denes | Implemented orphan murdering technique |
tree | commitdiff |
2009-06-29 |
Enrico Tassi | new make test target |
tree | commitdiff |
2009-06-26 |
Andrea Asperti | attempt to run a last chance procedure after the timeout |
tree | commitdiff |
2009-06-26 |
Andrea Asperti | the timeout is passed to test last chance |
tree | commitdiff |
2009-06-26 |
Andrea Asperti | this case is not assert false since it can happen if... |
tree | commitdiff |
2009-06-26 |
Andrea Asperti | fixed parsing |
tree | commitdiff |
2009-06-26 |
Andrea Asperti | convenient problem lists |
tree | commitdiff |
2009-06-26 |
Andrea Asperti | an easy for loop |
tree | commitdiff |
2009-06-26 |
Andrea Asperti | deep subsumption activated |
tree | commitdiff |
2009-06-26 |
denes | Implemented orphan murder test (clauses are not discard... |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | ... |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | better doc |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | timeouts are passed as arguments, so that tptpprover can |
tree | commitdiff |
2009-06-25 |
Ferruccio Guidi | - some depend files :) |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | the prover is almost OK, types in fuctors a bit extended to |
tree | commitdiff |
2009-06-25 |
Andrea Asperti | First version of deep_subsumption. |
tree | commitdiff |
2009-06-25 |
denes | Various fixes |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | new function |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | ... |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | matitaprover is almost there |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | ... |
tree | commitdiff |
next |