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

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

2009-07-31	denes	Fixed (yet another) nasty bug, in deep_eq this time	commit \| commitdiff \| tree
2009-07-31	denes	Fixed nasty bug in superposition and freshing of clauses	commit \| commitdiff \| tree
2009-07-31	denes	Now iterating superposition	commit \| commitdiff \| tree
2009-07-30	denes	Ported demodulation on clauses	commit \| commitdiff \| tree
2009-07-30	denes	Added check for trivial (identity) goal	commit \| commitdiff \| tree
2009-07-29	denes	Update eligible problem list (now sorted)	commit \| commitdiff \| tree
2009-07-29	denes	Added TreeLimitRun	commit \| commitdiff \| tree
2009-07-29	denes	Added Clauses module	commit \| commitdiff \| tree
2009-07-29	denes	Added symbolic link to clauses	commit \| commitdiff \| tree
2009-07-29	denes	Reorganized foUtils, added Clauses module to avoid...	commit \| commitdiff \| tree
2009-07-28	denes	Various architectural changes	commit \| commitdiff \| tree
2009-07-28	denes	Various architectural changes	commit \| commitdiff \| tree
2009-07-24	denes	Added symbolic links to hTopoSort	commit \| commitdiff \| tree
2009-07-24	denes	Fixed pretty printer and debug printings	commit \| commitdiff \| tree
2009-07-23	denes	First compiling version	commit \| commitdiff \| tree
2009-07-23	denes	Fixed useage	commit \| commitdiff \| tree
2009-07-22	denes	Fixes	commit \| commitdiff \| tree
2009-07-22	denes	Fixed conflicts due to problem when merging with UEQ...	commit \| commitdiff \| tree
2009-07-17	denes	Branched paramodulation for CNF (Horn clauses)	commit \| commitdiff \| tree
2009-07-15	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree
2009-07-14	denes	Fixed Option type error (OCaml bug)	commit \| commitdiff \| tree
2009-07-14	denes	.	commit \| commitdiff \| tree
2009-07-14	denes	.	commit \| commitdiff \| tree
2009-07-14	Cosimo Oliboni	freescale porting to ng, work in progress	commit \| commitdiff \| tree
2009-07-13	denes	Added statistics printings	commit \| commitdiff \| tree
2009-07-13	denes	Added statistics module	commit \| commitdiff \| tree
2009-07-13	Cosimo Oliboni	freescale translation (work in progress)	commit \| commitdiff \| tree
2009-07-12	Cosimo Oliboni	(no commit message)	commit \| commitdiff \| tree
2009-07-11	Cosimo Oliboni	(no commit message)	commit \| commitdiff \| tree
2009-07-10	Cosimo Oliboni	+root +depends	commit \| commitdiff \| tree
2009-07-10	denes	Removed unused parameter of unification procedure ...	commit \| commitdiff \| tree
2009-07-10	Cosimo Oliboni	new ng freescale, no external dependencies	commit \| commitdiff \| tree
2009-07-09	denes	Fixed check for condition iv p.33 (Riazzanov)	commit \| commitdiff \| tree
2009-07-09	denes	Cleaned a bit	commit \| commitdiff \| tree
2009-07-08	Cosimo Oliboni	directory for porting the assembly to matita-ng	commit \| commitdiff \| tree
2009-07-06	denes	Fixed printing of number of problems solved	commit \| commitdiff \| tree
2009-07-06	denes	Tried to implement lpo in a more efficient way	commit \| commitdiff \| tree
2009-07-06	denes	Fixed typo in lpo (from old implementation)	commit \| commitdiff \| tree
2009-07-03	denes	Ported old implementation of LPO (for test purposes)	commit \| commitdiff \| tree
2009-07-03	denes	Implemented LPO	commit \| commitdiff \| tree
2009-07-02	denes	Corrected type for bag	commit \| commitdiff \| tree
2009-07-02	denes	New age selection	commit \| commitdiff \| tree
2009-07-01	denes	Fixed type of bag	commit \| commitdiff \| tree
2009-06-30	denes	Moved ID management inside the bag	commit \| commitdiff \| tree
2009-06-30	denes	Corrected a few typos	commit \| commitdiff \| tree
2009-06-30	denes	Enabled age selection (ratio 1/5)	commit \| commitdiff \| tree
2009-06-29	denes	First attempt for refined goal selection strategy	commit \| commitdiff \| tree
2009-06-29	denes	Implemented orphan murdering technique	commit \| commitdiff \| tree
2009-06-26	denes	Implemented orphan murder test (clauses are not discarded...	commit \| commitdiff \| tree
2009-06-25	denes	Various fixes	commit \| commitdiff \| tree
2009-06-25	denes	Now using age selection	commit \| commitdiff \| tree
2009-06-25	denes	Fixed is_identity for facts	commit \| commitdiff \| tree
2009-06-25	denes	Fixed insertion of passive clauses	commit \| commitdiff \| tree
2009-06-24	denes	Removed debug printing	commit \| commitdiff \| tree
2009-06-24	denes	Now inserting hypothesis and goal with zero weight	commit \| commitdiff \| tree
2009-06-24	denes	Extended is_identity test	commit \| commitdiff \| tree
2009-06-24	denes	Implemented check for duplicates (in goals)	commit \| commitdiff \| tree
2009-06-23	denes	Removed old debugging assertion	commit \| commitdiff \| tree
2009-06-23	denes	Removed debug printing raising Failure	commit \| commitdiff \| tree
2009-06-23	denes	Removed debug printing	commit \| commitdiff \| tree
2009-06-23	denes	Rewrote the main loop for paramodulation	commit \| commitdiff \| tree
2009-06-23	denes	Fixed nasty bug in maxvar updating	commit \| commitdiff \| tree
2009-06-22	denes	Added more precise time information	commit \| commitdiff \| tree
2009-06-22	denes	Added problems from CASC 208	commit \| commitdiff \| tree
2009-06-22	denes	Regenerated problems with corrected tptp2grafite	commit \| commitdiff \| tree
2009-06-22	denes	Corrected proof visiting (topological sort)	commit \| commitdiff \| tree
2009-06-22	denes	Small debugging in tptp2grafite	commit \| commitdiff \| tree
2009-06-18	denes	Added ntry and nassumption tactics	commit \| commitdiff \| tree
2009-06-18	denes	Fixed stupid path	commit \| commitdiff \| tree
2009-06-18	denes	Added script useful for running benchmarks	commit \| commitdiff \| tree
2009-06-18	denes	Changed parenthesis to optional around letin ident...	commit \| commitdiff \| tree
2009-06-18	denes	Fixed wrong types in proof terms	commit \| commitdiff \| tree
2009-06-17	denes	Added optionnal one pass simplification (instead of...	commit \| commitdiff \| tree
2009-06-12	denes	Implemented keep_simplified.	commit \| commitdiff \| tree
2009-06-11	denes	Active goals are now demodulated after selecting a...	commit \| commitdiff \| tree
2009-06-10	denes	Extended the equality case to non ground terms	commit \| commitdiff \| tree
2009-06-09	denes	Optimized weigths comparison, removed normalization	commit \| commitdiff \| tree
2009-06-09	denes	Implemented substitution application and concatenation	commit \| commitdiff \| tree
2009-06-05	denes	First tests for paramodulation (pretty printer, unification)	commit \| commitdiff \| tree
2009-06-05	denes	Fix : wrong exception was catch in apply_subst	commit \| commitdiff \| tree
2009-06-04	denes	First pretty printing functions	commit \| commitdiff \| tree
2009-06-01	denes	First implementation of unification on foterms	commit \| commitdiff \| tree
2009-06-01	denes	First functions on substitutions for unification	commit \| commitdiff \| tree
2007-10-14	Cristian Armentano	Theorem sigma_p_knm changed into generic_iter_p_knm.	commit \| commitdiff \| tree
2007-09-20	Cristian Armentano	Further simplifications to the main theorem about Euler...	commit \| commitdiff \| tree
2007-09-19	Cristian Armentano	* Some simplifications to theorem in file totient1.ma.	commit \| commitdiff \| tree
2007-09-18	Cristian Armentano	some theorems have been moved to more appropriate files...	commit \| commitdiff \| tree
2007-09-17	Cristian Armentano	temporary changes, before the complete cancellation...	commit \| commitdiff \| tree
2007-09-17	Cristian Armentano	simplified version of a theorem.	commit \| commitdiff \| tree
2007-09-11	Cristian Armentano	some theorem names changed.	commit \| commitdiff \| tree
2007-09-10	Cristian Armentano	other simplifications.	commit \| commitdiff \| tree
2007-09-09	Cristian Armentano	other simplifications.	commit \| commitdiff \| tree
2007-09-07	Cristian Armentano	some simplifications.	commit \| commitdiff \| tree
2007-09-06	Cristian Armentano	Some simplifications.	commit \| commitdiff \| tree
2007-08-16	Cristian Armentano	little change to theorem eq_gcd_times_times_eqv_times_gcd	commit \| commitdiff \| tree
2007-07-30	Cristian Armentano	renamed generic_sigma_p.ma to generic_iter_p.ma	commit \| commitdiff \| tree
2007-06-30	Cristian Armentano	New definition of Euler's totient function.	commit \| commitdiff \| tree
2007-06-29	Cristian Armentano	generic version, specializing generic_sigma_p.ma	commit \| commitdiff \| tree
2007-06-29	Cristian Armentano	generic version	commit \| commitdiff \| tree
2007-06-29	Cristian Armentano	theorems about sigma_p proved using sigma_p_gen	commit \| commitdiff \| tree
next

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

RSS Atom