| 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 |
| 2007-06-27 |
Cristian Armentano | new gcd properties, and theorems for totient, and theorems...
|
commit | commitdiff | tree |
| 2007-06-26 |
Cristian Armentano | (no commit message)
|
commit | commitdiff | tree |
| 2007-06-26 |
Cristian Armentano | generic sommatory.
|
commit | commitdiff | tree |
| 2007-05-18 |
lzingare | added alternative implementation for hMysql relying
|
commit | commitdiff | tree |
| 2007-04-20 |
Cristian Armentano | changed base uri
|
commit | commitdiff | tree |
| 2007-04-20 |
Cristian Armentano | initial import
|
commit | commitdiff | tree |
| 2007-03-01 |
Enrico Zoli | "by j let x : T such that P(x)" generalized to allow...
|
commit | commitdiff | tree |
| 2007-02-20 |
notin | small fix to make it compile again
|
commit | commitdiff | tree |
| 2007-01-17 |
Enrico Zoli | This is the roadmap of the constructive proof of Lebesgue...
|
commit | commitdiff | tree |
| 2006-12-15 |
Enrico Zoli | Up to definition of limsup as liminf computed on the...
|
commit | commitdiff | tree |
| 2006-12-15 |
Enrico Zoli | Fatou lemma achieved (up to a few more axioms here...
|
commit | commitdiff | tree |
| 2006-11-14 |
maiorino | New: on-line help for declarative tactics (first version).
|
commit | commitdiff | tree |
| 2006-11-10 |
Enrico Zoli | Dama: up to L-spaces and the proof (completed up to...
|
commit | commitdiff | tree |
| 2006-11-06 |
Enrico Zoli | More work on groups, real numbers and integration algebras.
|
commit | commitdiff | tree |
| 2006-11-03 |
Enrico Zoli | Integration f_algebras declassed.
|
commit | commitdiff | tree |
| 2006-11-03 |
Enrico Zoli | Up to absolute value
|
commit | commitdiff | tree |
| 2006-11-03 |
Enrico Zoli | Up to max (up to a bug).
|
commit | commitdiff | tree |
| 2006-10-31 |
Enrico Zoli | We begin to play the real game: we have defined real...
|
commit | commitdiff | tree |
| next |
projects / helm.git / search