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

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

2009-09-25	denes	Ported innermost strategy for demodulation from trunk	commit \| commitdiff \| tree
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-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-13	denes	Added statistics printings	commit \| commitdiff \| tree
2009-07-13	denes	Added statistics module	commit \| commitdiff \| tree
2009-07-10	denes	Removed unused parameter of unification procedure ...	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-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

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

RSS Atom