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

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

2010-03-17	Andrea Asperti	Aggiornamento alla negazione.	commit \| commitdiff \| tree
2010-03-17	Andrea Asperti	Nuova definizione della negazione.	commit \| commitdiff \| tree
2010-03-12	Andrea Asperti	First version of PTS	commit \| commitdiff \| tree
2010-03-12	Andrea Asperti	New definition of negation	commit \| commitdiff \| tree
2010-03-12	Andrea Asperti	Subst was missing in perforate small (apparently, gty...	commit \| commitdiff \| tree
2010-03-12	Andrea Asperti	removed debug from the inteface	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	In line with the ml.	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	1. For smart application, we only perforate small terms...	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	Small changes for debugging	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	Fixed a bug in deep_eq: we generated new clauses but...	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	Corrected a bug relative to the application of substs...	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Open goals fixed (it also returned closed goals).	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Removed debug printings.	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	added lazy	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Nuova versione di auto.	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	New proofs.	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Wilmer's stuff for destruct.	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	(no commit message)	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	commit \| commitdiff \| tree
2010-02-16	Andrea Asperti	More theorems	commit \| commitdiff \| tree
2010-02-16	Andrea Asperti	Minor fixings.	commit \| commitdiff \| tree
2010-02-10	Andrea Asperti	addenda	commit \| commitdiff \| tree
2010-02-09	Andrea Asperti	Added a count_occurrences function.	commit \| commitdiff \| tree
2010-02-08	Andrea Asperti	Bug fixing.	commit \| commitdiff \| tree
2010-02-08	Andrea Asperti	Removed debug printings.	commit \| commitdiff \| tree
2010-02-08	Andrea Asperti	Some changes towards integration of setoid-rewriting.	commit \| commitdiff \| tree
2010-02-04	Andrea Asperti	Added count_occurrences.	commit \| commitdiff \| tree
2010-02-04	Andrea Asperti	Bug fixed: goto_top used to reset the status to the...	commit \| commitdiff \| tree
2010-02-02	Andrea Asperti	lists	commit \| commitdiff \| tree
2010-02-02	Andrea Asperti	Booleans	commit \| commitdiff \| tree
2010-02-02	Andrea Asperti	boolean arithmetics	commit \| commitdiff \| tree
2010-02-01	Andrea Asperti	minus	commit \| commitdiff \| tree
2010-02-01	Andrea Asperti	On the last goal at maxdepth we stop at the first solution.	commit \| commitdiff \| tree
2010-01-29	Andrea Asperti	minus in nat.ma	commit \| commitdiff \| tree
2010-01-29	Andrea Asperti	Nuova gestione della width.	commit \| commitdiff \| tree
2010-01-27	Andrea Asperti	le_arith	commit \| commitdiff \| tree
2010-01-27	Andrea Asperti	Unfolded exact letins during proof reconstruction.	commit \| commitdiff \| tree
2010-01-27	Andrea Asperti	Added a parameter no_implicit (default true) to choose...	commit \| commitdiff \| tree
2010-01-26	Andrea Asperti	le_arith	commit \| commitdiff \| tree
2010-01-21	Andrea Asperti	Esempio	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	New paramod tac.	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Invocation of paramod	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	paramod_tac exported	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Number notation for NG	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Number notation for NG	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Number notation for NG.	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Keeping Implicit for refinement (instead of transforming...	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Updating.	commit \| commitdiff \| tree
2010-01-11	Andrea Asperti	1. New paramodulation function	commit \| commitdiff \| tree
2010-01-11	Andrea Asperti	saturate cust be called with delta=0	commit \| commitdiff \| tree
2010-01-11	Andrea Asperti	Added is_equation	commit \| commitdiff \| tree
2010-01-11	Andrea Asperti	Debugging info	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	The body of constants is a reference, not the actual...	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	removed debugging info	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	applyS	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	refresh uri	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	Support for the new auto tactics //	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	Support for the new // tactics.	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	new reloc_subst (to avoid cyclic substitutions).	commit \| commitdiff \| tree
2009-12-21	Andrea Asperti	Refining with no expected type + unification seems...	commit \| commitdiff \| tree
2009-12-21	Andrea Asperti	Trying to be faster	commit \| commitdiff \| tree
2009-12-21	Andrea Asperti	Trying to be faster.	commit \| commitdiff \| tree
2009-12-18	Andrea Asperti	Final subst returned by superposition and passed around.	commit \| commitdiff \| tree
2009-12-18	Andrea Asperti	using = instead of alpha conversions. context metasenv...	commit \| commitdiff \| tree
2009-12-15	Andrea Asperti	eq_coerc for smart application.	commit \| commitdiff \| tree
2009-12-10	Andrea Asperti	Minor bag fixed, relative to failures.	commit \| commitdiff \| tree
2009-12-10	Andrea Asperti	A compiling version?	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Added a "sort_metasenv" function.	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Commented a couple of calls to "set_reference_of_oxuri".	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Added the paramodulation stuff to the status	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	param "slir" to call the new auto	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Added the paramodulation active/passive tables to the...	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Attached fast_eq_check to auto	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Added nnAuto.mli	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Debug set to ()	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Clean up of debgging info	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Syntax error	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Wrong reference corrected	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Minor fixing for last chance	commit \| commitdiff \| tree
2009-12-09	Andrea Asperti	Added a fol operation	commit \| commitdiff \| tree
2009-12-04	Andrea Asperti	Indexing local context for paramod.	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	Propositional equality	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	The new paramodulation functions instantiated over...	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	New ways for initialising the signature required for...	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	Passive equations have their own index (not passive...	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	debug takes lazy strings. Moved here the are_alpha_eq...	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	Added a function remove_unit_clause	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	Added a boolean test function to discriminate equations...	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	Generalized intitialization for EqP	commit \| commitdiff \| tree
2009-12-02	Andrea Asperti	Generalized initialization of eqP.	commit \| commitdiff \| tree
2009-11-25	Andrea Asperti	Exported forward_inference_step	commit \| commitdiff \| tree
2009-11-23	Andrea Asperti	Removed dead code	commit \| commitdiff \| tree
2009-11-23	Andrea Asperti	Subsumption and reduction	commit \| commitdiff \| tree
2009-11-17	Andrea Asperti	Closing the goal.	commit \| commitdiff \| tree
2009-11-13	Andrea Asperti	Exported apply_subst_context	commit \| commitdiff \| tree
2009-11-13	Andrea Asperti	Added the new auto version (not attached yet).	commit \| commitdiff \| tree
2009-11-10	Andrea Asperti	Union find slightly more general (f can now point to...	commit \| commitdiff \| tree
next

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

RSS Atom