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

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

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
2007-11-19	Andrea Asperti	Towards chebyshev.	commit \| commitdiff \| tree
2007-10-12	Andrea Asperti	More restructuring in moebius.ma	commit \| commitdiff \| tree
2007-10-12	Andrea Asperti	Reorganization of the library.	commit \| commitdiff \| tree
2007-10-12	Andrea Asperti	Reorganization of the library.	commit \| commitdiff \| tree
2007-10-12	Andrea Asperti	Reorganization of results.	commit \| commitdiff \| tree
2007-10-08	Andrea Asperti	Some axioms for Q.	commit \| commitdiff \| tree
2007-09-17	Andrea Asperti	Some new lemmas.	commit \| commitdiff \| tree
2007-09-17	Andrea Asperti	A new function.	commit \| commitdiff \| tree
2007-09-14	Andrea Asperti	Qualche semplificazione.	commit \| commitdiff \| tree
2007-07-31	Andrea Asperti	removed generic_sigma_p since generic_iter_p is the...	commit \| commitdiff \| tree
2007-05-29	Andrea Asperti	Corrected version od meta_convertibnility_subst.	commit \| commitdiff \| tree
2007-05-28	Andrea Asperti	Improved pruning (no propress).	commit \| commitdiff \| tree
2007-05-28	Andrea Asperti	Added a new version of meta_convertibnility that returns the	commit \| commitdiff \| tree
2007-05-09	Andrea Asperti	A few extensions for the moebius inversion theorem	commit \| commitdiff \| tree
2007-05-09	Andrea Asperti	Proof of the moebius inversion theorem	commit \| commitdiff \| tree
2007-04-30	Andrea Asperti	Even if we are at depth 0, we first check in the cache...	commit \| commitdiff \| tree
2007-04-30	Andrea Asperti	Removed an assert false; everything works again, but...	commit \| commitdiff \| tree
2007-04-27	Andrea Asperti	Subst is passed in input to apapluy, so no need to...	commit \| commitdiff \| tree
2007-04-27	Andrea Asperti	Apply_with_subst now returns a subst with a correct...	commit \| commitdiff \| tree
2007-04-24	Andrea Asperti	Subsumption_subst re-added to initial.	commit \| commitdiff \| tree
2007-04-24	Andrea Asperti	@	commit \| commitdiff \| tree
2007-03-16	Andrea Asperti	New contrib moebius.ma.	commit \| commitdiff \| tree
2007-03-16	Andrea Asperti	Extensions required for the moebius function (in Z).	commit \| commitdiff \| tree
2007-03-13	Andrea Asperti	Few theorems added.`	commit \| commitdiff \| tree
2007-03-13	Andrea Asperti	new version of div_and_mod	commit \| commitdiff \| tree
next

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

RSS Atom