2009-07-29 |
denes | Added Clauses module |
tree | commitdiff |
2009-07-29 |
denes | Added symbolic link to clauses |
tree | commitdiff |
2009-07-29 |
denes | Reorganized foUtils, added Clauses module to avoid... |
tree | commitdiff |
2009-07-28 |
denes | Various architectural changes |
tree | commitdiff |
2009-07-28 |
denes | Various architectural changes |
tree | commitdiff |
2009-07-24 |
denes | Added symbolic links to hTopoSort |
tree | commitdiff |
2009-07-24 |
denes | Fixed pretty printer and debug printings |
tree | commitdiff |
2009-07-23 |
denes | First compiling version |
tree | commitdiff |
2009-07-23 |
denes | Fixed useage |
tree | commitdiff |
2009-07-22 |
denes | Fixes |
tree | commitdiff |
2009-07-22 |
denes | Fixed conflicts due to problem when merging with UEQ... |
tree | commitdiff |
2009-07-17 |
denes | Branched paramodulation for CNF (Horn clauses) |
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 |
2009-06-25 |
Enrico Tassi | initial import of standalone matitaprover binary |
tree | commitdiff |
2009-06-25 |
denes | Now using age selection |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | code refactoring for paramodulation |
tree | commitdiff |
2009-06-25 |
Enrico Tassi | new function list_mapi_acc |
tree | commitdiff |
2009-06-25 |
denes | Fixed is_identity for facts |
tree | commitdiff |
next |