| 2010-03-25 |
Andrea Asperti | Extension of demod to arbtrary predicates (not just... |
tree | commitdiff |
| 2010-03-24 |
Claudio Sacerdoti... | Axioms were not indexed. |
tree | commitdiff |
| 2010-03-24 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2010-03-23 |
Andrea Asperti | Fixed a few bugs |
tree | commitdiff |
| 2010-03-23 |
Andrea Asperti | "flat" function (subst unfolding) |
tree | commitdiff |
| 2010-03-18 |
Andrea Asperti | Debugging disabled. |
tree | commitdiff |
| 2010-03-18 |
Andrea Asperti | Exporting the demodulation function. |
tree | commitdiff |
| 2010-03-16 |
Claudio Sacerdoti... | Comparison of two applications with a different number... |
tree | commitdiff |
| 2010-03-04 |
Andrea Asperti | Small changes for debugging |
tree | commitdiff |
| 2010-03-04 |
Andrea Asperti | Fixed a bug in deep_eq: we generated new clauses but... |
tree | commitdiff |
| 2010-03-04 |
Andrea Asperti | Corrected a bug relative to the application of substs... |
tree | commitdiff |
| 2010-02-19 |
Andrea Asperti | Added an implicit parameter to branch_tac to allow... |
tree | commitdiff |
| 2010-02-08 |
Andrea Asperti | Some changes towards integration of setoid-rewriting. |
tree | commitdiff |
| 2010-02-03 |
Claudio Sacerdoti... | Debug code commented out. |
tree | commitdiff |
| 2010-01-27 |
Andrea Asperti | Unfolded exact letins during proof reconstruction. |
tree | commitdiff |
| 2010-01-18 |
Andrea Asperti | Keeping Implicit for refinement (instead of transformin... |
tree | commitdiff |
| 2010-01-11 |
Andrea Asperti | 1. New paramodulation function |
tree | commitdiff |
| 2010-01-11 |
Andrea Asperti | saturate cust be called with delta=0 |
tree | commitdiff |
| 2010-01-11 |
Andrea Asperti | Added is_equation |
tree | commitdiff |
| 2010-01-11 |
Andrea Asperti | Debugging info |
tree | commitdiff |
| 2010-01-08 |
Andrea Asperti | The body of constants is a reference, not the actual... |
tree | commitdiff |
| 2010-01-08 |
Andrea Asperti | removed debugging info |
tree | commitdiff |
| 2010-01-08 |
Andrea Asperti | new reloc_subst (to avoid cyclic substitutions). |
tree | commitdiff |
| 2009-12-21 |
Andrea Asperti | Trying to be faster |
tree | commitdiff |
| 2009-12-18 |
Andrea Asperti | Final subst returned by superposition and passed around. |
tree | commitdiff |
| 2009-12-18 |
Andrea Asperti | using = instead of alpha conversions. context metasenv... |
tree | commitdiff |
| 2009-12-09 |
Andrea Asperti | Debug set to () |
tree | commitdiff |
| 2009-12-09 |
Andrea Asperti | Clean up of debgging info |
tree | commitdiff |
| 2009-12-09 |
Andrea Asperti | Syntax error |
tree | commitdiff |
| 2009-12-09 |
Andrea Asperti | Wrong reference corrected |
tree | commitdiff |
| 2009-12-09 |
Andrea Asperti | Minor fixing for last chance |
tree | commitdiff |
| 2009-12-09 |
Andrea Asperti | Added a fol operation |
tree | commitdiff |
| 2009-12-02 |
Andrea Asperti | The new paramodulation functions instantiated over... |
tree | commitdiff |
| 2009-12-02 |
Andrea Asperti | New ways for initialising the signature required for... |
tree | commitdiff |
| 2009-12-02 |
Andrea Asperti | Passive equations have their own index (not passive... |
tree | commitdiff |
| 2009-12-02 |
Andrea Asperti | debug takes lazy strings. Moved here the are_alpha_eq... |
tree | commitdiff |
| 2009-12-02 |
Andrea Asperti | Added a function remove_unit_clause |
tree | commitdiff |
| 2009-12-02 |
Andrea Asperti | Added a boolean test function to discriminate equations... |
tree | commitdiff |
| 2009-12-02 |
Andrea Asperti | Generalized intitialization for EqP |
tree | commitdiff |
| 2009-12-02 |
Andrea Asperti | Generalized initialization of eqP. |
tree | commitdiff |
| 2009-11-25 |
Andrea Asperti | Exported forward_inference_step |
tree | commitdiff |
| 2009-11-23 |
Andrea Asperti | Removed dead code |
tree | commitdiff |
| 2009-11-16 |
Wilmer Ricciotti | Implementation of ndestruct tactic (including destructi... |
tree | commitdiff |
| 2009-10-22 |
Enrico Tassi | new instantiate, only known bug is w.r.t. in/out scope... |
tree | commitdiff |
| 2009-10-07 |
Claudio Sacerdoti... | - oCic2NCic and nCic2OCic moved to ng_library |
tree | commitdiff |
| 2009-10-06 |
Wilmer Ricciotti | Inverters/Inversion: |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | added auto_cache in the dupable status after an |
tree | commitdiff |
| 2009-10-02 |
Wilmer Ricciotti | Updated command ninverter. Syntax: |
tree | commitdiff |
| 2009-10-02 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-09-30 |
Wilmer Ricciotti | Added initial support for inversion principles in Matit... |
tree | commitdiff |
| 2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | depends |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | some more work for ng-coercions |
tree | commitdiff |
| 2009-07-29 |
Andrea Asperti | New demodulation (innermost, optimized to avoid reducin... |
tree | commitdiff |
| 2009-07-29 |
Andrea Asperti | Changed the ordering of rels, and the introduction... |
tree | commitdiff |
| 2009-07-29 |
Andrea Asperti | Lazy strings |
tree | commitdiff |
| 2009-07-27 |
denes | Removed meaningless time information |
tree | commitdiff |
| 2009-07-22 |
denes | Fixed test for invertibility |
tree | commitdiff |
| 2009-07-22 |
denes | Now using lazy strings for debug printings |
tree | commitdiff |
| 2009-07-21 |
denes | Implemented handling of Invertible equalities |
tree | commitdiff |
| 2009-07-20 |
Enrico Tassi | sorted modules |
tree | commitdiff |
| 2009-07-20 |
Wilmer Ricciotti | added a flag for age selection |
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-16 |
denes | Disabled age selection and ad hoc goal weight computation |
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 |
| next |
projects / helm.git / history