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

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

[helm.git] / helm / software / components /

2009-07-24	denes	Fixed pretty printer and debug printings	tree \| commitdiff
2009-07-23	denes	First compiling version	tree \| commitdiff
2009-07-23	denes	Fixed useage	tree \| commitdiff
2009-07-22	denes	Fixes	tree \| commitdiff
2009-07-22	denes	Fixed conflicts due to problem when merging with UEQ...	tree \| commitdiff
2009-07-17	denes	Branched paramodulation for CNF (Horn clauses)	tree \| commitdiff
2009-07-15	Enrico Tassi	ncopy partially implemented and fixed (a ?) chain to...	tree \| commitdiff
2009-07-15	Wilmer Ricciotti	Fixed dependency function, which was lacking the code...	tree \| commitdiff
2009-07-15	Enrico Tassi	...	tree \| commitdiff
2009-07-15	Enrico Tassi	match_coercion gives back the saturations, not the...	tree \| commitdiff
2009-07-14	denes	Fixed Option type error (OCaml bug)	tree \| commitdiff
2009-07-14	denes	.	tree \| commitdiff
2009-07-14	denes	.	tree \| commitdiff
2009-07-13	Enrico Tassi	better spacing	tree \| commitdiff
2009-07-13	Enrico Tassi	statistics are used, when possible, to sort	tree \| commitdiff
2009-07-13	denes	Added statistics printings	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-13	Claudio Sacerdoti...	Coercion hiding implemented. Notes:	tree \| commitdiff
2009-07-10	Enrico Tassi	initial implementation of coercion composition	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-10	Claudio Sacerdoti...	Bug fixed (missing ctx) + comment added.	tree \| commitdiff
2009-07-09	Enrico Tassi	initial implementation of `ncoercion name : type :...	tree \| commitdiff
2009-07-09	Enrico Tassi	new nrepeat (and block '('...')' ) tactical	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	1 process for now	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	...	tree \| commitdiff
2009-07-09	Enrico Tassi	activate kbo, not lpo	tree \| commitdiff
2009-07-09	Claudio Sacerdoti...	Bug fixed (non-captured variable).	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	repeat_tac	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	Metavariable case in does_not_occur (hence weakly/stric...	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	Missing case for Match implemented.	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	weakly/strictly positive checks relaxed to allow metava...	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	Improved error message.	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	Bug fixed: the debrujinate function (hence the one...	tree \| commitdiff
2009-07-07	Claudio Sacerdoti...	Bug fixed: one uri was not refreshed, causing divergenc...	tree \| commitdiff
2009-07-07	Claudio Sacerdoti...	1) Include files for NG were neither recursively proces...	tree \| commitdiff
2009-07-06	denes	Fixed printing of number of problems solved	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	Corrected type for bag	tree \| commitdiff
2009-07-02	denes	New age selection	tree \| commitdiff
2009-07-02	Enrico Tassi	better output handling	tree \| commitdiff
2009-07-02	Enrico Tassi	return type of paramod fixed according to the SZSOntology	tree \| commitdiff
2009-07-01	Enrico Tassi	...	tree \| commitdiff
2009-07-01	Enrico Tassi	...	tree \| commitdiff
2009-07-01	Wilmer Ricciotti	Version number set to 1.0.0-rc1	tree \| commitdiff
2009-07-01	denes	Fixed type of bag	tree \| commitdiff
2009-06-30	Enrico Tassi	parallel	tree \| commitdiff
2009-06-30	denes	Moved ID management inside the bag	tree \| commitdiff
2009-06-30	Enrico Tassi	attempt of using 2 different orderings	tree \| commitdiff
2009-06-30	Enrico Tassi	....	tree \| commitdiff
2009-06-30	denes	Corrected a few typos	tree \| commitdiff
2009-06-30	Enrico Tassi	...	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	Enrico Tassi	...	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-29	Enrico Tassi	new make test target	tree \| commitdiff
2009-06-26	Andrea Asperti	attempt to run a last chance procedure after the timeout	tree \| commitdiff
2009-06-26	Andrea Asperti	the timeout is passed to test last chance	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	fixed parsing	tree \| commitdiff
2009-06-26	Andrea Asperti	convenient problem lists	tree \| commitdiff
2009-06-26	Andrea Asperti	an easy for loop	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	...	tree \| commitdiff
2009-06-25	Enrico Tassi	better doc	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
2009-06-25	Enrico Tassi	the prover is almost OK, types in fuctors a bit extended to	tree \| commitdiff
2009-06-25	Andrea Asperti	First version of deep_subsumption.	tree \| commitdiff
2009-06-25	denes	Various fixes	tree \| commitdiff
2009-06-25	Enrico Tassi	new function	tree \| commitdiff
2009-06-25	Enrico Tassi	...	tree \| commitdiff
2009-06-25	Enrico Tassi	matitaprover is almost there	tree \| commitdiff
2009-06-25	Enrico Tassi	...	tree \| commitdiff
2009-06-25	Enrico Tassi	initial import of standalone matitaprover binary	tree \| commitdiff
2009-06-25	denes	Now using age selection	tree \| commitdiff
2009-06-25	Enrico Tassi	code refactoring for paramodulation	tree \| commitdiff
2009-06-25	Enrico Tassi	new function list_mapi_acc	tree \| commitdiff
2009-06-25	denes	Fixed is_identity for facts	tree \| commitdiff
2009-06-25	denes	Fixed insertion of passive clauses	tree \| commitdiff
2009-06-25	Andrea Asperti	Code factorization	tree \| commitdiff
2009-06-24	denes	Removed debug printing	tree \| commitdiff
2009-06-24	denes	Now inserting hypothesis and goal with zero weight	tree \| commitdiff
2009-06-24	denes	Extended is_identity test	tree \| commitdiff
2009-06-24	denes	Implemented check for duplicates (in goals)	tree \| commitdiff
next

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

RSS Atom