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

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

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
2009-05-05	Andrea Asperti	Nuova gestione di "by" per auto.	commit \| commitdiff \| tree
2009-05-05	Andrea Asperti	autobatch by	commit \| commitdiff \| tree
2009-04-30	Andrea Asperti	Minor changes pro-automation	commit \| commitdiff \| tree
2009-04-30	Andrea Asperti	Added a passive table	commit \| commitdiff \| tree
2009-04-30	Andrea Asperti	Calling paramodulation instead of demod_all	commit \| commitdiff \| tree
2009-03-16	Andrea Asperti	New parameters for applyS: 10 20.	commit \| commitdiff \| tree
2009-03-16	Andrea Asperti	Adapted to new applyS.	commit \| commitdiff \| tree
2009-03-16	Andrea Asperti	Added a property.	commit \| commitdiff \| tree
2009-03-10	Andrea Asperti	A version of applyS with bounded iterations of given_clause...	commit \| commitdiff \| tree
2009-03-10	Andrea Asperti	Removed the context from the metasenv to avoid trivial...	commit \| commitdiff \| tree
2009-02-12	Andrea Asperti	errata corrige.	commit \| commitdiff \| tree
2009-02-12	Andrea Asperti	Fixed a problem of lifting.	commit \| commitdiff \| tree
2008-11-07	Andrea Asperti	debug=false	commit \| commitdiff \| tree
2008-11-07	Andrea Asperti	Signature_of has been closed with respect to constructors.	commit \| commitdiff \| tree
2008-11-07	Andrea Asperti	The signature in "retrieve equations" must be extended...	commit \| commitdiff \| tree
2008-11-04	Andrea Asperti	Calling unification instead of matching when checking...	commit \| commitdiff \| tree
2008-10-29	Andrea Asperti	Propagation of changes in paramodulation.	commit \| commitdiff \| tree
2008-10-29	Andrea Asperti	Exported a couple of functions.	commit \| commitdiff \| tree
2008-10-29	Andrea Asperti	Added a in_universe function	commit \| commitdiff \| tree
2008-10-29	Andrea Asperti	propagation of changes in other paramodulation files.	commit \| commitdiff \| tree
2008-10-29	Andrea Asperti	New demod function working for arbitary goals.	commit \| commitdiff \| tree
2008-10-29	Andrea Asperti	Enforcing the disjoint invariant between metasenvs.	commit \| commitdiff \| tree
2008-10-29	Andrea Asperti	Main change: added a parameter to build_equality_proof...	commit \| commitdiff \| tree
2008-09-19	Andrea Asperti	A temporary patch to demodulation theorem.	commit \| commitdiff \| tree
2008-06-06	Andrea Asperti	A new theorem	commit \| commitdiff \| tree
2008-06-06	Andrea Asperti	cleanup	commit \| commitdiff \| tree
2008-06-06	Andrea Asperti	Cleanup.	commit \| commitdiff \| tree
2008-06-06	Andrea Asperti	Added frac.ma	commit \| commitdiff \| tree
2008-06-06	Andrea Asperti	Added Qplus_andrea.ma	commit \| commitdiff \| tree
2008-05-15	Andrea Asperti	Removed two args from psubst.	commit \| commitdiff \| tree
2008-03-12	Andrea Asperti	Nuova dimostrazione riflessiva di le_to_Bertrand.	commit \| commitdiff \| tree
2008-02-19	Andrea Asperti	Added o.ma (some results about the magnitude of functions *)	commit \| commitdiff \| tree
2008-02-18	Andrea Asperti	Complete proof of Bertrand for n >= 256.	commit \| commitdiff \| tree
2008-02-14	Andrea Asperti	Prima versione di bertrand. Tanti cambiamenti qua e la.	commit \| commitdiff \| tree
2008-02-08	Andrea Asperti	progress.	commit \| commitdiff \| tree
2008-02-07	Andrea Asperti	Results about Chebyshev teta function.	commit \| commitdiff \| tree
2008-02-05	Andrea Asperti	Some more theorems.	commit \| commitdiff \| tree
2008-02-04	Andrea Asperti	Improved approximations for A and prim.	commit \| commitdiff \| tree
2008-02-04	Andrea Asperti	Some improvement.	commit \| commitdiff \| tree
2008-01-30	Andrea Asperti	Improved approximations	commit \| commitdiff \| tree
2008-01-29	Andrea Asperti	New approximtions.	commit \| commitdiff \| tree
2007-12-17	Andrea Asperti	A few more lemmas.	commit \| commitdiff \| tree
2007-12-13	Andrea Asperti	Some inequalities.	commit \| commitdiff \| tree
2007-12-11	Andrea Asperti	Partial progress.	commit \| commitdiff \| tree
2007-12-10	Andrea Asperti	Main result for e.	commit \| commitdiff \| tree
2007-12-10	Andrea Asperti	Restructuring.	commit \| commitdiff \| tree
2007-12-10	Andrea Asperti	Main inequalities for e.	commit \| commitdiff \| tree
2007-12-07	Andrea Asperti	Binomial coefficients and costant e.	commit \| commitdiff \| tree
2007-12-07	Andrea Asperti	A few more theorems.	commit \| commitdiff \| tree
2007-12-03	Andrea Asperti	Some progress.	commit \| commitdiff \| tree
2007-11-26	Andrea Asperti	Almost there.	commit \| commitdiff \| tree
2007-11-22	Andrea Asperti	Big progress	commit \| commitdiff \| tree
next

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

RSS Atom