matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_paramodulation/orderings.ml

[helm.git] / helm / software / components / ng_paramodulation / orderings.ml

2009-07-22	denes	Fixed test for invertibility	blob \| commitdiff \| raw
2009-07-21	denes	Implemented handling of Invertible equalities	blob \| commitdiff \| raw \| diff to current
2009-07-20	denes	One-side indexing for commutativity	blob \| commitdiff \| raw \| diff to current
2009-07-16	denes	Disabled age selection and ad hoc goal weight computation	blob \| commitdiff \| raw \| diff to current
2009-07-09	Enrico Tassi	New functorialization: paramod is abstracted over a...	blob \| commitdiff \| raw \| diff to current
2009-07-09	Enrico Tassi	two cases should be assert false at least in TPTP	blob \| commitdiff \| raw \| diff to current
2009-07-09	denes	Cleaned a bit	blob \| commitdiff \| raw \| diff to current
2009-07-09	Enrico Tassi	activate kbo, not lpo	blob \| commitdiff \| raw \| diff to current
2009-07-06	denes	Tried to implement lpo in a more efficient way	blob \| commitdiff \| raw \| diff to current
2009-07-06	denes	Fixed typo in lpo (from old implementation)	blob \| commitdiff \| raw \| diff to current
2009-07-03	denes	Ported old implementation of LPO (for test purposes)	blob \| commitdiff \| raw \| diff to current
2009-07-03	denes	Implemented LPO	blob \| commitdiff \| raw \| diff to current
2009-06-29	denes	First attempt for refined goal selection strategy	blob \| commitdiff \| raw \| diff to current
2009-06-11	denes	Active goals are now demodulated after selecting a...	blob \| commitdiff \| raw \| diff to current
2009-06-10	denes	Extended the equality case to non ground terms	blob \| commitdiff \| raw \| diff to current
2009-06-09	denes	Optimized weigths comparison, removed normalization	blob \| commitdiff \| raw \| diff to current
2009-06-09	Enrico Tassi	snaphost: supright almost done	blob \| commitdiff \| raw \| diff to current
2009-06-04	Enrico Tassi	better type for comparison and implementation of KBO...	blob \| commitdiff \| raw \| diff to current
2009-06-03	Enrico Tassi	functorial abstraction over term blobs	blob \| commitdiff \| raw \| diff to current
2009-06-01	Enrico Tassi	added a snapshot of comparison	blob \| commitdiff \| raw \| diff to current
2009-06-01	Enrico Tassi	we rewrite the paramodulation code!	blob \| commitdiff \| raw \| diff to current

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

RSS Atom