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

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

2009-07-10	Enrico Tassi	more profilers	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	Coercions used here and there.	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	Bug fixed (missing ctx) + comment added.	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-10	Cosimo Oliboni	new ng freescale, no external dependencies	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	Let's live with new ocaml type system limitations...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	initial implementation of `ncoercion name : type :...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	claudio, please have a look at this	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	new nrepeat (and block '('...')' ) tactical	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	New functorialization: paramod is abstracted over a...	commit \| commitdiff \| tree \| snapshot
2009-07-09	denes	Fixed check for condition iv p.33 (Riazzanov)	commit \| commitdiff \| tree \| snapshot
2009-07-09	Wilmer Ricciotti	More updates to Fsub.	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	profile most operations, do not return a filtered varli...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	1 process for now	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	two cases should be assert false at least in TPTP	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	micro optimizations to unification	commit \| commitdiff \| tree \| snapshot
2009-07-09	denes	Cleaned a bit	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	activate kbo, not lpo	commit \| commitdiff \| tree \| snapshot
2009-07-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Claudio Sacerdoti...	Bug fixed (non-captured variable).	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	eq moved to CProp	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	repeat_tac	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Enrico Tassi	few more files, one diverges	commit \| commitdiff \| tree \| snapshot
2009-07-08	Cosimo Oliboni	directory for porting the assembly to matita-ng	commit \| commitdiff \| tree \| snapshot
2009-07-08	Enrico Tassi	removed useless universes	commit \| commitdiff \| tree \| snapshot
2009-07-08	Enrico Tassi	import of a sample for cosimo	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Hmmmm. This way we need "canonical structures" also...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Metavariable case in does_not_occur (hence weakly/stric...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Missing case for Match implemented.	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	weakly/strictly positive checks relaxed to allow metava...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Improved error message.	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Bug fixed: the debrujinate function (hence the one...	commit \| commitdiff \| tree \| snapshot
2009-07-07	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-07	Claudio Sacerdoti...	Bug fixed: one uri was not refreshed, causing divergenc...	commit \| commitdiff \| tree \| snapshot
2009-07-07	Enrico Tassi	fixed some typos	commit \| commitdiff \| tree \| snapshot
2009-07-07	Claudio Sacerdoti...	Let's play a bit with NG.	commit \| commitdiff \| tree \| snapshot
2009-07-07	Claudio Sacerdoti...	1) Include files for NG were neither recursively proces...	commit \| commitdiff \| tree \| snapshot
2009-07-06	denes	Fixed printing of number of problems solved	commit \| commitdiff \| tree \| snapshot
2009-07-06	denes	Tried to implement lpo in a more efficient way	commit \| commitdiff \| tree \| snapshot
2009-07-06	denes	Fixed typo in lpo (from old implementation)	commit \| commitdiff \| tree \| snapshot
2009-07-03	Ferruccio Guidi	some corrections	commit \| commitdiff \| tree \| snapshot
2009-07-03	Ferruccio Guidi	more static analysis on the Automath text	commit \| commitdiff \| tree \| snapshot
2009-07-03	denes	Ported old implementation of LPO (for test purposes)	commit \| commitdiff \| tree \| snapshot
2009-07-03	Ferruccio Guidi	we now do some static analysis on the Automath text...	commit \| commitdiff \| tree \| snapshot
2009-07-03	denes	Implemented LPO	commit \| commitdiff \| tree \| snapshot
2009-07-02	denes	Corrected type for bag	commit \| commitdiff \| tree \| snapshot
2009-07-02	denes	New age selection	commit \| commitdiff \| tree \| snapshot
2009-07-02	Enrico Tassi	better output handling	commit \| commitdiff \| tree \| snapshot
2009-07-02	Enrico Tassi	return type of paramod fixed according to the SZSOntology	commit \| commitdiff \| tree \| snapshot
2009-07-01	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-07-01	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-07-01	Wilmer Ricciotti	Version number set to 1.0.0-rc1	commit \| commitdiff \| tree \| snapshot
2009-07-01	denes	Fixed type of bag	commit \| commitdiff \| tree \| snapshot
2009-06-30	Enrico Tassi	parallel	commit \| commitdiff \| tree \| snapshot
2009-06-30	denes	Moved ID management inside the bag	commit \| commitdiff \| tree \| snapshot
2009-06-30	Enrico Tassi	attempt of using 2 different orderings	commit \| commitdiff \| tree \| snapshot
2009-06-30	Enrico Tassi	....	commit \| commitdiff \| tree \| snapshot
2009-06-30	denes	Corrected a few typos	commit \| commitdiff \| tree \| snapshot
2009-06-30	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-30	denes	Enabled age selection (ratio 1/5)	commit \| commitdiff \| tree \| snapshot
2009-06-29	Ferruccio Guidi	lambda-delta:	commit \| commitdiff \| tree \| snapshot
2009-06-29	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-29	Enrico Tassi	do not infer on closed goals	commit \| commitdiff \| tree \| snapshot
2009-06-29	Enrico Tassi	removed a maybe diverging test	commit \| commitdiff \| tree \| snapshot
2009-06-29	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-29	denes	First attempt for refined goal selection strategy	commit \| commitdiff \| tree \| snapshot
2009-06-29	Enrico Tassi	added (but not active) last chance idea	commit \| commitdiff \| tree \| snapshot
2009-06-29	denes	Implemented orphan murdering technique	commit \| commitdiff \| tree \| snapshot
2009-06-29	Enrico Tassi	new make test target	commit \| commitdiff \| tree \| snapshot
2009-06-28	Ferruccio Guidi	new kernel basic_rg: implements ufficial lambda-delta...	commit \| commitdiff \| tree \| snapshot
2009-06-26	Andrea Asperti	attempt to run a last chance procedure after the timeout	commit \| commitdiff \| tree \| snapshot
2009-06-26	Andrea Asperti	the timeout is passed to test last chance	commit \| commitdiff \| tree \| snapshot
2009-06-26	Andrea Asperti	this case is not assert false since it can happen if...	commit \| commitdiff \| tree \| snapshot
2009-06-26	Andrea Asperti	fixed parsing	commit \| commitdiff \| tree \| snapshot
2009-06-26	Andrea Asperti	convenient problem lists	commit \| commitdiff \| tree \| snapshot
2009-06-26	Andrea Asperti	an easy for loop	commit \| commitdiff \| tree \| snapshot
2009-06-26	Andrea Asperti	deep subsumption activated	commit \| commitdiff \| tree \| snapshot
2009-06-26	Andrea Asperti	test for deep subsumption added	commit \| commitdiff \| tree \| snapshot
2009-06-26	denes	Implemented orphan murder test (clauses are not discard...	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	better doc	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	timeouts are passed as arguments, so that tptpprover can	commit \| commitdiff \| tree \| snapshot
2009-06-25	Ferruccio Guidi	- some depend files :)	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	the prover is almost OK, types in fuctors a bit extended to	commit \| commitdiff \| tree \| snapshot
2009-06-25	Andrea Asperti	First version of deep_subsumption.	commit \| commitdiff \| tree \| snapshot
2009-06-25	denes	Various fixes	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	new function	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	matitaprover is almost there	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	initial import of standalone matitaprover binary	commit \| commitdiff \| tree \| snapshot
2009-06-25	denes	Now using age selection	commit \| commitdiff \| tree \| snapshot
2009-06-25	Enrico Tassi	code refactoring for paramodulation	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom