matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_paramodulation/superposition.mli

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

projects / helm.git / history

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

[helm.git] / helm / software / components / ng_paramodulation / superposition.mli

2009-06-29	denes	Implemented orphan murdering technique	blob \| commitdiff \| raw
2009-06-26	Andrea Asperti	attempt to run a last chance procedure after the timeout	blob \| commitdiff \| raw \| diff to current
2009-06-26	denes	Implemented orphan murder test (clauses are not discard...	blob \| commitdiff \| raw \| diff to current
2009-06-25	denes	Various fixes	blob \| commitdiff \| raw \| diff to current
2009-06-24	denes	Implemented check for duplicates (in goals)	blob \| commitdiff \| raw \| diff to current
2009-06-18	denes	Fixed wrong types in proof terms	blob \| commitdiff \| raw \| diff to current
2009-06-17	denes	Added optionnal one pass simplification (instead of...	blob \| commitdiff \| raw \| diff to current
2009-06-12	denes	Implemented keep_simplified.	blob \| commitdiff \| raw \| diff to current
2009-06-12	Andrea Asperti	Renamed forward_simplify into simplify and backward_sim...	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	Enrico Tassi	1) added simplification of actives w.r.t. selected	blob \| commitdiff \| raw \| diff to current
2009-06-10	Enrico Tassi	right inference step completed	blob \| commitdiff \| raw \| diff to current
2009-06-09	Enrico Tassi	almost complete superposition right step	blob \| commitdiff \| raw \| diff to current
2009-06-09	Enrico Tassi	snaphost: supright almost done	blob \| commitdiff \| raw \| diff to current
2009-06-08	Enrico Tassi	some more functors and a nice higher-order all_position...	blob \| commitdiff \| raw \| diff to current

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