matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_paramodulation

[helm.git] / helm / software / components / ng_paramodulation /

2010-04-19	Andrea Asperti	alpha_eq instead of pervasives.compare	tree \| commitdiff
2010-04-13	Enrico Tassi	same heads different arity -> INCOMPARABLE	tree \| commitdiff
2010-03-25	Andrea Asperti	Extension of demod to arbtrary predicates (not just...	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	...	tree \| commitdiff
2010-03-23	Andrea Asperti	Fixed a few bugs	tree \| commitdiff
2010-03-23	Andrea Asperti	"flat" function (subst unfolding)	tree \| commitdiff
2010-03-18	Andrea Asperti	Debugging disabled.	tree \| commitdiff
2010-03-18	Andrea Asperti	Exporting the demodulation function.	tree \| commitdiff
2010-03-16	Claudio Sacerdoti...	Comparison of two applications with a different number...	tree \| commitdiff
2010-03-04	Andrea Asperti	Small changes for debugging	tree \| commitdiff
2010-03-04	Andrea Asperti	Fixed a bug in deep_eq: we generated new clauses but...	tree \| commitdiff
2010-03-04	Andrea Asperti	Corrected a bug relative to the application of substs...	tree \| commitdiff
2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	tree \| commitdiff
2010-02-08	Andrea Asperti	Some changes towards integration of setoid-rewriting.	tree \| commitdiff
2010-02-03	Claudio Sacerdoti...	Debug code commented out.	tree \| commitdiff
2010-01-27	Andrea Asperti	Unfolded exact letins during proof reconstruction.	tree \| commitdiff
2010-01-18	Andrea Asperti	Keeping Implicit for refinement (instead of transformin...	tree \| commitdiff
2010-01-11	Andrea Asperti	1. New paramodulation function	tree \| commitdiff
2010-01-11	Andrea Asperti	saturate cust be called with delta=0	tree \| commitdiff
2010-01-11	Andrea Asperti	Added is_equation	tree \| commitdiff
2010-01-11	Andrea Asperti	Debugging info	tree \| commitdiff
2010-01-08	Andrea Asperti	The body of constants is a reference, not the actual...	tree \| commitdiff
2010-01-08	Andrea Asperti	removed debugging info	tree \| commitdiff
2010-01-08	Andrea Asperti	new reloc_subst (to avoid cyclic substitutions).	tree \| commitdiff
2009-12-21	Andrea Asperti	Trying to be faster	tree \| commitdiff
2009-12-18	Andrea Asperti	Final subst returned by superposition and passed around.	tree \| commitdiff
2009-12-18	Andrea Asperti	using = instead of alpha conversions. context metasenv...	tree \| commitdiff
2009-12-09	Andrea Asperti	Debug set to ()	tree \| commitdiff
2009-12-09	Andrea Asperti	Clean up of debgging info	tree \| commitdiff
2009-12-09	Andrea Asperti	Syntax error	tree \| commitdiff
2009-12-09	Andrea Asperti	Wrong reference corrected	tree \| commitdiff
2009-12-09	Andrea Asperti	Minor fixing for last chance	tree \| commitdiff
2009-12-09	Andrea Asperti	Added a fol operation	tree \| commitdiff
2009-12-02	Andrea Asperti	The new paramodulation functions instantiated over...	tree \| commitdiff
2009-12-02	Andrea Asperti	New ways for initialising the signature required for...	tree \| commitdiff
2009-12-02	Andrea Asperti	Passive equations have their own index (not passive...	tree \| commitdiff
2009-12-02	Andrea Asperti	debug takes lazy strings. Moved here the are_alpha_eq...	tree \| commitdiff
2009-12-02	Andrea Asperti	Added a function remove_unit_clause	tree \| commitdiff
2009-12-02	Andrea Asperti	Added a boolean test function to discriminate equations...	tree \| commitdiff
2009-12-02	Andrea Asperti	Generalized intitialization for EqP	tree \| commitdiff
2009-12-02	Andrea Asperti	Generalized initialization of eqP.	tree \| commitdiff
2009-11-25	Andrea Asperti	Exported forward_inference_step	tree \| commitdiff
2009-11-23	Andrea Asperti	Removed dead code	tree \| commitdiff
2009-11-16	Wilmer Ricciotti	Implementation of ndestruct tactic (including destructi...	tree \| commitdiff
2009-10-22	Enrico Tassi	new instantiate, only known bug is w.r.t. in/out scope...	tree \| commitdiff
2009-10-07	Claudio Sacerdoti...	- oCic2NCic and nCic2OCic moved to ng_library	tree \| commitdiff
2009-10-06	Wilmer Ricciotti	Inverters/Inversion:	tree \| commitdiff
2009-10-05	Enrico Tassi	added auto_cache in the dupable status after an	tree \| commitdiff
2009-10-02	Wilmer Ricciotti	Updated command ninverter. Syntax:	tree \| commitdiff
2009-10-02	Claudio Sacerdoti...	...	tree \| commitdiff
2009-09-30	Wilmer Ricciotti	Added initial support for inversion principles in Matit...	tree \| commitdiff
2009-09-21	Enrico Tassi	huge commit regarding universes:	tree \| commitdiff
2009-09-09	Enrico Tassi	depends	tree \| commitdiff
2009-09-09	Enrico Tassi	some more work for ng-coercions	tree \| commitdiff
2009-07-29	Andrea Asperti	New demodulation (innermost, optimized to avoid reducin...	tree \| commitdiff
2009-07-29	Andrea Asperti	Changed the ordering of rels, and the introduction...	tree \| commitdiff
2009-07-29	Andrea Asperti	Lazy strings	tree \| commitdiff
2009-07-27	denes	Removed meaningless time information	tree \| commitdiff
2009-07-22	denes	Fixed test for invertibility	tree \| commitdiff
2009-07-22	denes	Now using lazy strings for debug printings	tree \| commitdiff
2009-07-21	denes	Implemented handling of Invertible equalities	tree \| commitdiff
2009-07-20	Enrico Tassi	sorted modules	tree \| commitdiff
2009-07-20	Wilmer Ricciotti	added a flag for age selection	tree \| commitdiff
2009-07-20	denes	One-side indexing for commutativity	tree \| commitdiff
2009-07-20	denes	No demod call on functionnal symbols	tree \| commitdiff
2009-07-16	denes	Disabled age selection and ad hoc goal weight computation	tree \| commitdiff
2009-07-15	Wilmer Ricciotti	Fixed dependency function, which was lacking the code...	tree \| commitdiff
2009-07-14	denes	.	tree \| commitdiff
2009-07-14	denes	.	tree \| commitdiff
2009-07-13	Enrico Tassi	statistics are used, when possible, to sort	tree \| commitdiff
2009-07-13	denes	Added statistics module	tree \| commitdiff
2009-07-13	Enrico Tassi	matitaprover is now flexible enough to allow the comput...	tree \| commitdiff
2009-07-10	denes	Removed unused parameter of unification procedure ...	tree \| commitdiff
2009-07-10	Enrico Tassi	more profilers	tree \| commitdiff
2009-07-09	Enrico Tassi	New functorialization: paramod is abstracted over a...	tree \| commitdiff
2009-07-09	denes	Fixed check for condition iv p.33 (Riazzanov)	tree \| commitdiff
2009-07-09	Enrico Tassi	profile most operations, do not return a filtered varli...	tree \| commitdiff
2009-07-09	Enrico Tassi	two cases should be assert false at least in TPTP	tree \| commitdiff
2009-07-09	Enrico Tassi	micro optimizations to unification	tree \| commitdiff
2009-07-09	denes	Cleaned a bit	tree \| commitdiff
2009-07-09	Enrico Tassi	activate kbo, not lpo	tree \| commitdiff
2009-07-07	Claudio Sacerdoti...	1) Include files for NG were neither recursively proces...	tree \| commitdiff
2009-07-06	denes	Tried to implement lpo in a more efficient way	tree \| commitdiff
2009-07-06	denes	Fixed typo in lpo (from old implementation)	tree \| commitdiff
2009-07-03	denes	Ported old implementation of LPO (for test purposes)	tree \| commitdiff
2009-07-03	denes	Implemented LPO	tree \| commitdiff
2009-07-02	denes	New age selection	tree \| commitdiff
2009-07-02	Enrico Tassi	return type of paramod fixed according to the SZSOntology	tree \| commitdiff
2009-06-30	denes	Moved ID management inside the bag	tree \| commitdiff
2009-06-30	denes	Enabled age selection (ratio 1/5)	tree \| commitdiff
2009-06-29	Enrico Tassi	...	tree \| commitdiff
2009-06-29	Enrico Tassi	do not infer on closed goals	tree \| commitdiff
2009-06-29	denes	First attempt for refined goal selection strategy	tree \| commitdiff
2009-06-29	Enrico Tassi	added (but not active) last chance idea	tree \| commitdiff
2009-06-29	denes	Implemented orphan murdering technique	tree \| commitdiff
2009-06-26	Andrea Asperti	attempt to run a last chance procedure after the timeout	tree \| commitdiff
2009-06-26	Andrea Asperti	this case is not assert false since it can happen if...	tree \| commitdiff
2009-06-26	Andrea Asperti	deep subsumption activated	tree \| commitdiff
2009-06-26	denes	Implemented orphan murder test (clauses are not discard...	tree \| commitdiff
next

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

RSS Atom