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

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

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
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
next

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

RSS Atom