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

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

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
2009-11-05	Andrea Asperti	A case was missing	commit \| commitdiff \| tree
2009-11-05	Andrea Asperti	Naif version of the union find	commit \| commitdiff \| tree
2009-07-29	Andrea Asperti	New demodulation (innermost, optimized to avoid reducing...	commit \| commitdiff \| tree
2009-07-29	Andrea Asperti	Changed the ordering of rels, and the introduction...	commit \| commitdiff \| tree
2009-07-29	Andrea Asperti	Lazy strings	commit \| commitdiff \| tree
2009-07-29	Andrea Asperti	Added the benchmark with the new demodulation function.	commit \| commitdiff \| tree
2009-06-26	Andrea Asperti	attempt to run a last chance procedure after the timeout	commit \| commitdiff \| tree
2009-06-26	Andrea Asperti	the timeout is passed to test last chance	commit \| commitdiff \| tree
2009-06-26	Andrea Asperti	this case is not assert false since it can happen if...	commit \| commitdiff \| tree
2009-06-26	Andrea Asperti	fixed parsing	commit \| commitdiff \| tree
2009-06-26	Andrea Asperti	convenient problem lists	commit \| commitdiff \| tree
2009-06-26	Andrea Asperti	an easy for loop	commit \| commitdiff \| tree
2009-06-26	Andrea Asperti	deep subsumption activated	commit \| commitdiff \| tree
2009-06-26	Andrea Asperti	test for deep subsumption added	commit \| commitdiff \| tree
2009-06-25	Andrea Asperti	First version of deep_subsumption.	commit \| commitdiff \| tree
2009-06-25	Andrea Asperti	Code factorization	commit \| commitdiff \| tree
2009-06-12	Andrea Asperti	Added a new keep_simplified function	commit \| commitdiff \| tree
2009-06-12	Andrea Asperti	Renamed forward_simplify into simplify and backward_simplify	commit \| commitdiff \| tree
2009-06-03	Andrea Asperti	not_to_not	commit \| commitdiff \| tree
2009-06-01	Andrea Asperti	This works for me	commit \| commitdiff \| tree
2009-05-27	Andrea Asperti	Avoiding to filter the application of congruence equations	commit \| commitdiff \| tree
2009-05-26	Andrea Asperti	removed a call to autobatch.	commit \| commitdiff \| tree
2009-05-22	Andrea Asperti	Pruning candidates in the applicative case for equalities.	commit \| commitdiff \| tree
2009-05-21	Andrea Asperti	autobatch -> autobatch by	commit \| commitdiff \| tree
2009-05-20	Andrea Asperti	Removed a silly type check	commit \| commitdiff \| tree
2009-05-19	Andrea Asperti	NotEq is now considered as a negative Eq atom	commit \| commitdiff \| tree
2009-05-13	Andrea Asperti	The singature of the "by" universe is added to the...	commit \| commitdiff \| tree
2009-05-13	Andrea Asperti	Via un'altra linea...	commit \| commitdiff \| tree
2009-05-13	Andrea Asperti	Sempre piu' breve	commit \| commitdiff \| tree
2009-05-13	Andrea Asperti	Signature is computed on the initial goal, once and...	commit \| commitdiff \| tree
2009-05-12	Andrea Asperti	We only filter the smart candidates w.r.t the signature	commit \| commitdiff \| tree
2009-05-11	Andrea Asperti	A few lemmas about inclusion.	commit \| commitdiff \| tree
2009-05-11	Andrea Asperti	More automation	commit \| commitdiff \| tree
2009-05-08	Andrea Asperti	Constructors are closed with thier types when computing...	commit \| commitdiff \| tree
2009-05-08	Andrea Asperti	versione automatizzata	commit \| commitdiff \| tree
2009-05-08	Andrea Asperti	symmetry of inequality sym_neq	commit \| commitdiff \| tree
next

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

RSS Atom