2008-11-06 |
Enrico Tassi | added some news |
commit | commitdiff | tree | snapshot |
2008-11-06 |
Enrico Tassi | almost ok |
commit | commitdiff | tree | snapshot |
2008-11-06 |
Enrico Tassi | natural deduction support and example split, seems... |
commit | commitdiff | tree | snapshot |
2008-11-06 |
Enrico Tassi | do not erase sorts |
commit | commitdiff | tree | snapshot |
2008-11-06 |
Enrico Tassi | better error messages. sorts are compared using whd |
commit | commitdiff | tree | snapshot |
2008-11-06 |
Enrico Tassi | Evil case fixed, the coulde should be more readable |
commit | commitdiff | tree | snapshot |
2008-11-06 |
Enrico Tassi | removed empty lines |
commit | commitdiff | tree | snapshot |
2008-11-06 |
Enrico Tassi | the passive set and passive list are expected to have... |
commit | commitdiff | tree | snapshot |
2008-11-06 |
Enrico Tassi | fixed scripts |
commit | commitdiff | tree | snapshot |
2008-11-05 |
Enrico Tassi | still some glitches, but reaching a decent state |
commit | commitdiff | tree | snapshot |
2008-11-05 |
Enrico Tassi | using the new by foo we proved semantics |
commit | commitdiff | tree | snapshot |
2008-11-05 |
Enrico Tassi | new internal flags for auto: |
commit | commitdiff | tree | snapshot |
2008-11-05 |
Enrico Tassi | duplicate entry in menv avoided |
commit | commitdiff | tree | snapshot |
2008-11-05 |
Enrico Tassi | fixed script to use auto depth=4 |
commit | commitdiff | tree | snapshot |
2008-11-04 |
Enrico Tassi | eliminazione di un passaggio di transitività in ast2astfe |
commit | commitdiff | tree | snapshot |
2008-11-04 |
Andrea Asperti | Calling unification instead of matching when checking... |
commit | commitdiff | tree | snapshot |
2008-11-04 |
Claudio Sacerdoti... | - A new interesting elimination principle over inductiv... |
commit | commitdiff | tree | snapshot |
2008-11-03 |
Enrico Tassi | BDD |
commit | commitdiff | tree | snapshot |
2008-11-03 |
Enrico Tassi | removed prerr_endline |
commit | commitdiff | tree | snapshot |
2008-11-03 |
Enrico Tassi | debug=false |
commit | commitdiff | tree | snapshot |
2008-11-02 |
Enrico Tassi | shannon proved |
commit | commitdiff | tree | snapshot |
2008-11-01 |
Enrico Tassi | added shannon |
commit | commitdiff | tree | snapshot |
2008-11-01 |
Enrico Tassi | added lazy |
commit | commitdiff | tree | snapshot |
2008-10-31 |
Claudio Sacerdoti... | Environment simplified. |
commit | commitdiff | tree | snapshot |
2008-10-31 |
Claudio Sacerdoti... | No longer used. |
commit | commitdiff | tree | snapshot |
2008-10-31 |
Claudio Sacerdoti... | - New dependency for environments on the nesting depth. |
commit | commitdiff | tree | snapshot |
2008-10-29 |
Andrea Asperti | Propagation of changes in paramodulation. |
commit | commitdiff | tree | snapshot |
2008-10-29 |
Andrea Asperti | Exported a couple of functions. |
commit | commitdiff | tree | snapshot |
2008-10-29 |
Andrea Asperti | Added a in_universe function |
commit | commitdiff | tree | snapshot |
2008-10-29 |
Andrea Asperti | propagation of changes in other paramodulation files. |
commit | commitdiff | tree | snapshot |
2008-10-29 |
Andrea Asperti | New demod function working for arbitary goals. |
commit | commitdiff | tree | snapshot |
2008-10-29 |
Enrico Tassi | models ported |
commit | commitdiff | tree | snapshot |
2008-10-29 |
Andrea Asperti | Enforcing the disjoint invariant between metasenvs. |
commit | commitdiff | tree | snapshot |
2008-10-29 |
Andrea Asperti | Main change: added a parameter to build_equality_proof... |
commit | commitdiff | tree | snapshot |
2008-10-28 |
Enrico Tassi | even more polymorphic dualizer |
commit | commitdiff | tree | snapshot |
2008-10-28 |
Enrico Tassi | done |
commit | commitdiff | tree | snapshot |
2008-10-28 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-28 |
Enrico Tassi | lebesge works |
commit | commitdiff | tree | snapshot |
2008-10-27 |
Enrico Tassi | WIP |
commit | commitdiff | tree | snapshot |
2008-10-27 |
Enrico Tassi | many bugs fixed |
commit | commitdiff | tree | snapshot |
2008-10-27 |
Enrico Tassi | metasenv passed to get_relevance, Metas that stand... |
commit | commitdiff | tree | snapshot |
2008-10-27 |
Enrico Tassi | WIP |
commit | commitdiff | tree | snapshot |
2008-10-27 |
Enrico Tassi | _ in place of unused variables |
commit | commitdiff | tree | snapshot |
2008-10-27 |
Enrico Tassi | Implicit annotationas are now printed |
commit | commitdiff | tree | snapshot |
2008-10-27 |
Enrico Tassi | seg_u/l were inverted, more work |
commit | commitdiff | tree | snapshot |
2008-10-27 |
Enrico Tassi | big lemma done |
commit | commitdiff | tree | snapshot |
2008-10-26 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-26 |
Enrico Tassi | duality done |
commit | commitdiff | tree | snapshot |
2008-10-26 |
Enrico Tassi | almost done, just needs to be prforated |
commit | commitdiff | tree | snapshot |
2008-10-26 |
Enrico Tassi | .... |
commit | commitdiff | tree | snapshot |
2008-10-26 |
Enrico Tassi | all done in declarative style |
commit | commitdiff | tree | snapshot |
2008-10-25 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-25 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-25 |
Enrico Tassi | duality is a joke |
commit | commitdiff | tree | snapshot |
2008-10-24 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-24 |
Enrico Tassi | leave-environment axiom made true |
commit | commitdiff | tree | snapshot |
2008-10-23 |
Enrico Tassi | lebesgue completely dualized |
commit | commitdiff | tree | snapshot |
2008-10-22 |
Ferruccio Guidi | we aligned the implementation to the plmms08 paper |
commit | commitdiff | tree | snapshot |
2008-10-21 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-21 |
Enrico Tassi | better pps |
commit | commitdiff | tree | snapshot |
2008-10-21 |
Enrico Tassi | - mk_restricted_irl removed, the non-optimized code... |
commit | commitdiff | tree | snapshot |
2008-10-21 |
Enrico Tassi | psubst for metas fixed again |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | nat model ported to the dualized version, but not itsel... |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | ... is a command in proof mode, use |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | more bug fixed (or introduced) |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | after a PITA, lebergue is dualized! |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-20 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-19 |
Enrico Tassi | some work on duality, still not finisched |
commit | commitdiff | tree | snapshot |
2008-10-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-19 |
Enrico Tassi | grave notation mistake fixed |
commit | commitdiff | tree | snapshot |
2008-10-19 |
Enrico Tassi | more tests |
commit | commitdiff | tree | snapshot |
2008-10-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-19 |
Enrico Tassi | when a file is opened the cursor is moved to the begin... |
commit | commitdiff | tree | snapshot |
2008-10-18 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-18 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-18 |
Enrico Tassi | tactic language documented; |
commit | commitdiff | tree | snapshot |
2008-10-18 |
Ferruccio Guidi | Acic2Procedural: |
commit | commitdiff | tree | snapshot |
2008-10-18 |
Enrico Tassi | html documentation generation implemented |
commit | commitdiff | tree | snapshot |
2008-10-18 |
Enrico Tassi | more doc |
commit | commitdiff | tree | snapshot |
2008-10-18 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-17 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-17 |
Enrico Tassi | new command eval added |
commit | commitdiff | tree | snapshot |
2008-10-17 |
Enrico Tassi | better makefile |
commit | commitdiff | tree | snapshot |
2008-10-17 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-16 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2008-10-16 |
Enrico Tassi | ex for students about induction |
commit | commitdiff | tree | snapshot |
2008-10-15 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-10-15 |
Enrico Tassi | delifting a Meta with an IRL w.r.t. another IRL complet... |
commit | commitdiff | tree | snapshot |
2008-10-15 |
Enrico Tassi | some bug fixed |
commit | commitdiff | tree | snapshot |
2008-10-15 |
Enrico Tassi | subst_meta was missing |
commit | commitdiff | tree | snapshot |
2008-10-15 |
Claudio Sacerdoti... | minor simplification + deps fixed |
commit | commitdiff | tree | snapshot |
2008-10-15 |
Claudio Sacerdoti... | New invariant and data structure to represent environme... |
commit | commitdiff | tree | snapshot |
2008-10-14 |
Enrico Tassi | more work |
commit | commitdiff | tree | snapshot |
next |