| 2009-07-24 |
denes | Fixed pretty printer and debug printings |
tree | commitdiff |
| 2009-07-23 |
denes | First compiling version |
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 |
Wilmer Ricciotti | Fixed dependency function, which was lacking the code... |
tree | commitdiff |
| 2009-07-14 |
denes | . |
tree | commitdiff |
| 2009-07-14 |
denes | . |
tree | commitdiff |
| 2009-07-13 |
Enrico Tassi | statistics are used, when possible, to sort |
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-10 |
denes | Removed unused parameter of unification procedure ... |
tree | commitdiff |
| 2009-07-10 |
Enrico Tassi | more profilers |
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 | 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 | activate kbo, not lpo |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
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 | New age selection |
tree | commitdiff |
| 2009-07-02 |
Enrico Tassi | return type of paramod fixed according to the SZSOntology |
tree | commitdiff |
| 2009-06-30 |
denes | Moved ID management inside the bag |
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 |
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-26 |
Andrea Asperti | attempt to run a last chance procedure after the timeout |
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 | deep subsumption activated |
tree | commitdiff |
| 2009-06-26 |
denes | Implemented orphan murder test (clauses are not discard... |
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 | matitaprover is almost there |
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 |
denes | Fixed is_identity for facts |
tree | commitdiff |
| 2009-06-25 |
denes | Fixed insertion of passive clauses |
tree | commitdiff |
| 2009-06-25 |
Andrea Asperti | Code factorization |
tree | commitdiff |
| 2009-06-24 |
denes | Removed debug printing |
tree | commitdiff |
| 2009-06-24 |
denes | Now inserting hypothesis and goal with zero weight |
tree | commitdiff |
| 2009-06-24 |
denes | Extended is_identity test |
tree | commitdiff |
| 2009-06-24 |
denes | Implemented check for duplicates (in goals) |
tree | commitdiff |
| 2009-06-23 |
denes | Removed old debugging assertion |
tree | commitdiff |
| 2009-06-23 |
denes | Removed debug printing raising Failure |
tree | commitdiff |
| 2009-06-23 |
denes | Removed debug printing |
tree | commitdiff |
| 2009-06-23 |
denes | Rewrote the main loop for paramodulation |
tree | commitdiff |
| 2009-06-23 |
denes | Fixed nasty bug in maxvar updating |
tree | commitdiff |
| 2009-06-22 |
denes | Added more precise time information |
tree | commitdiff |
| 2009-06-22 |
denes | Corrected proof visiting (topological sort) |
tree | commitdiff |
| 2009-06-18 |
Enrico Tassi | debug pps removed |
tree | commitdiff |
| 2009-06-18 |
Enrico Tassi | proof patching! |
tree | commitdiff |
| 2009-06-18 |
denes | Fixed wrong types in proof terms |
tree | commitdiff |
| 2009-06-17 |
Enrico Tassi | proof reconstruction almost OK |
tree | commitdiff |
| 2009-06-17 |
Claudio Sacerdoti... | Initial implementation of statuses using objects in... |
tree | commitdiff |
| 2009-06-17 |
denes | Added optionnal one pass simplification (instead of... |
tree | commitdiff |
| 2009-06-16 |
Enrico Tassi | first proof reconstruction attempt, still bugged since it |
tree | commitdiff |
| 2009-06-12 |
denes | Implemented keep_simplified. |
tree | commitdiff |
| 2009-06-12 |
Andrea Asperti | Added a new keep_simplified function |
tree | commitdiff |
| 2009-06-12 |
Andrea Asperti | Renamed forward_simplify into simplify and backward_sim... |
tree | commitdiff |
| 2009-06-11 |
denes | Active goals are now demodulated after selecting a... |
tree | commitdiff |
| 2009-06-11 |
Ferruccio Guidi | - some depend files fixed |
tree | commitdiff |
| 2009-06-10 |
Enrico Tassi | 1) added simplification of actives w.r.t. selected |
tree | commitdiff |
| 2009-06-10 |
Enrico Tassi | right inference step completed |
tree | commitdiff |
| 2009-06-10 |
denes | Extended the equality case to non ground terms |
tree | commitdiff |
| 2009-06-09 |
Enrico Tassi | almost complete superposition right step |
tree | commitdiff |
| 2009-06-09 |
Enrico Tassi | snapshot |
tree | commitdiff |
| 2009-06-09 |
denes | Optimized weigths comparison, removed normalization |
tree | commitdiff |
| 2009-06-09 |
Enrico Tassi | snaphost: supright almost done |
tree | commitdiff |
| 2009-06-09 |
denes | Implemented substitution application and concatenation |
tree | commitdiff |
| 2009-06-09 |
Enrico Tassi | fixed building |
tree | commitdiff |
| 2009-06-08 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-06-08 |
Enrico Tassi | a skeleton of supright |
tree | commitdiff |
| 2009-06-08 |
Enrico Tassi | some more functors and a nice higher-order all_position... |
tree | commitdiff |
| 2009-06-06 |
Enrico Tassi | some renaming to make ocamlopt happy |
tree | commitdiff |
| 2009-06-05 |
Ferruccio Guidi | - Procedural convertible rewrites in the conclusion... |
tree | commitdiff |
| 2009-06-05 |
denes | First tests for paramodulation (pretty printer, unifica... |
tree | commitdiff |
| 2009-06-04 |
denes | First pretty printing functions |
tree | commitdiff |
| 2009-06-04 |
Enrico Tassi | minor changes here and there. We extend fo-unification... |
tree | commitdiff |
| 2009-06-04 |
Enrico Tassi | comments |
tree | commitdiff |
| 2009-06-04 |
Enrico Tassi | better type for comparison and implementation of KBO... |
tree | commitdiff |
| 2009-06-04 |
Enrico Tassi | more functors |
tree | commitdiff |
| 2009-06-03 |
Enrico Tassi | functorial abstraction over term blobs |
tree | commitdiff |
| 2009-06-01 |
denes | First implementation of unification on foterms |
tree | commitdiff |
| 2009-06-01 |
denes | First functions on substitutions for unification |
tree | commitdiff |
| 2009-06-01 |
Enrico Tassi | added a snapshot of comparison |
tree | commitdiff |
| 2009-06-01 |
Enrico Tassi | we rewrite the paramodulation code! |
tree | commitdiff |
|
projects / helm.git / history