matita.cs.unibo.it Git - helm.git/search

]> matita.cs.unibo.it Git - helm.git/search

2009-07-06	denes	Tried to implement lpo in a more efficient way	commit \| commitdiff \| tree
2009-07-06	denes	Fixed typo in lpo (from old implementation)	commit \| commitdiff \| tree
2009-07-03	denes	Ported old implementation of LPO (for test purposes)	commit \| commitdiff \| tree
2009-07-03	denes	Implemented LPO	commit \| commitdiff \| tree
2009-07-02	denes	Corrected type for bag	commit \| commitdiff \| tree
2009-07-02	denes	New age selection	commit \| commitdiff \| tree
2009-07-01	denes	Fixed type of bag	commit \| commitdiff \| tree
2009-06-30	denes	Moved ID management inside the bag	commit \| commitdiff \| tree
2009-06-30	denes	Corrected a few typos	commit \| commitdiff \| tree
2009-06-30	denes	Enabled age selection (ratio 1/5)	commit \| commitdiff \| tree
2009-06-29	denes	First attempt for refined goal selection strategy	commit \| commitdiff \| tree
2009-06-29	denes	Implemented orphan murdering technique	commit \| commitdiff \| tree
2009-06-26	denes	Implemented orphan murder test (clauses are not discarded...	commit \| commitdiff \| tree
2009-06-25	denes	Various fixes	commit \| commitdiff \| tree
2009-06-25	denes	Now using age selection	commit \| commitdiff \| tree
2009-06-25	denes	Fixed is_identity for facts	commit \| commitdiff \| tree
2009-06-25	denes	Fixed insertion of passive clauses	commit \| commitdiff \| tree
2009-06-24	denes	Removed debug printing	commit \| commitdiff \| tree
2009-06-24	denes	Now inserting hypothesis and goal with zero weight	commit \| commitdiff \| tree
2009-06-24	denes	Extended is_identity test	commit \| commitdiff \| tree
2009-06-24	denes	Implemented check for duplicates (in goals)	commit \| commitdiff \| tree
2009-06-23	denes	Removed old debugging assertion	commit \| commitdiff \| tree
2009-06-23	denes	Removed debug printing raising Failure	commit \| commitdiff \| tree
2009-06-23	denes	Removed debug printing	commit \| commitdiff \| tree
2009-06-23	denes	Rewrote the main loop for paramodulation	commit \| commitdiff \| tree
2009-06-23	denes	Fixed nasty bug in maxvar updating	commit \| commitdiff \| tree
2009-06-22	denes	Added more precise time information	commit \| commitdiff \| tree
2009-06-22	denes	Added problems from CASC 208	commit \| commitdiff \| tree
2009-06-22	denes	Regenerated problems with corrected tptp2grafite	commit \| commitdiff \| tree
2009-06-22	denes	Corrected proof visiting (topological sort)	commit \| commitdiff \| tree
2009-06-22	denes	Small debugging in tptp2grafite	commit \| commitdiff \| tree
2009-06-18	denes	Added ntry and nassumption tactics	commit \| commitdiff \| tree
2009-06-18	denes	Fixed stupid path	commit \| commitdiff \| tree
2009-06-18	denes	Added script useful for running benchmarks	commit \| commitdiff \| tree
2009-06-18	denes	Changed parenthesis to optional around letin ident...	commit \| commitdiff \| tree
2009-06-18	denes	Fixed wrong types in proof terms	commit \| commitdiff \| tree
2009-06-17	denes	Added optionnal one pass simplification (instead of...	commit \| commitdiff \| tree
2009-06-12	denes	Implemented keep_simplified.	commit \| commitdiff \| tree
2009-06-11	denes	Active goals are now demodulated after selecting a...	commit \| commitdiff \| tree
2009-06-10	denes	Extended the equality case to non ground terms	commit \| commitdiff \| tree
2009-06-09	denes	Optimized weigths comparison, removed normalization	commit \| commitdiff \| tree
2009-06-09	denes	Implemented substitution application and concatenation	commit \| commitdiff \| tree
2009-06-05	denes	First tests for paramodulation (pretty printer, unification)	commit \| commitdiff \| tree
2009-06-05	denes	Fix : wrong exception was catch in apply_subst	commit \| commitdiff \| tree
2009-06-04	denes	First pretty printing functions	commit \| commitdiff \| tree
2009-06-01	denes	First implementation of unification on foterms	commit \| commitdiff \| tree
2009-06-01	denes	First functions on substitutions for unification	commit \| commitdiff \| tree

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom