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

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

2005-07-21	Alberto Griggio	modifications/fixes for the integration with auto	commit \| commitdiff \| tree
2005-07-21	Alberto Griggio	entry point of the stand-alone saturate	commit \| commitdiff \| tree
2005-07-21	Alberto Griggio	added paramodulation package	commit \| commitdiff \| tree
2005-07-18	Alberto Griggio	adding library support (not ready yet)	commit \| commitdiff \| tree
2005-07-11	Alberto Griggio	now proofs have the correct type :-)	commit \| commitdiff \| tree
2005-07-01	Alberto Griggio	fixed bug in proof generation, new weight function...	commit \| commitdiff \| tree
2005-07-01	Alberto Griggio	removed first Cic.term from type equality, added an...	commit \| commitdiff \| tree
2005-06-30	Alberto Griggio	proofs are now built lazily at the end of the computation	commit \| commitdiff \| tree
2005-06-29	Alberto Griggio	various updates, removed proofs for now because they...	commit \| commitdiff \| tree
2005-06-23	Alberto Griggio	added various profiling statistics...	commit \| commitdiff \| tree
2005-06-22	Alberto Griggio	reverted to previous version, as it worked better...	commit \| commitdiff \| tree
2005-06-22	Alberto Griggio	use of discrimination trees instead of path indexes...	commit \| commitdiff \| tree
2005-06-22	Alberto Griggio	trie structure implementation	commit \| commitdiff \| tree
2005-06-20	Alberto Griggio	some optimizations...	commit \| commitdiff \| tree
2005-06-20	Alberto Griggio	testing...	commit \| commitdiff \| tree
2005-06-20	Alberto Griggio	* empty log message *	commit \| commitdiff \| tree
2005-06-20	Alberto Griggio	discrimination trees	commit \| commitdiff \| tree
2005-06-19	Alberto Griggio	limited-resource-strategy implementation (now working!)	commit \| commitdiff \| tree
2005-06-19	Alberto Griggio	path indexing integration, limited-resource-strategy...	commit \| commitdiff \| tree
2005-06-19	Alberto Griggio	path indexing integration	commit \| commitdiff \| tree
2005-06-19	Alberto Griggio	path indexing working!	commit \| commitdiff \| tree
2005-06-17	Alberto Griggio	profiling experiments...	commit \| commitdiff \| tree
2005-06-15	Alberto Griggio	now something works...	commit \| commitdiff \| tree
2005-06-10	Alberto Griggio	integrated indexing.ml, breaks everything :-P (previous...	commit \| commitdiff \| tree
2005-06-09	Alberto Griggio	prima implementazione di demodulate, superposition_left...	commit \| commitdiff \| tree
2005-06-09	Alberto Griggio	cambiato il tipo equality, aggiunto l'ordinamento tra...	commit \| commitdiff \| tree
2005-06-07	Alberto Griggio	* empty log message *	commit \| commitdiff \| tree
2005-05-19	Alberto Griggio	added lpo term-ordering	commit \| commitdiff \| tree
2005-05-19	Alberto Griggio	various optimizations (to paramodulation and passive...	commit \| commitdiff \| tree
2005-05-15	Alberto Griggio	added saturation.opt to the ignore list	commit \| commitdiff \| tree
2005-05-15	Alberto Griggio	fixes (mainly) to demodulation and meta_convertibility	commit \| commitdiff \| tree
2005-05-13	Alberto Griggio	exported new_metasenv_for_apply, needed by the paramodulatio...	commit \| commitdiff \| tree
2005-05-13	Alberto Griggio	fixed demodulation bug	commit \| commitdiff \| tree
2005-05-13	Alberto Griggio	moved string_of_equality into utils	commit \| commitdiff \| tree
2005-05-12	Alberto Griggio	first commit of paramodulation-based theorem proving...	commit \| commitdiff \| tree

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

RSS Atom