| 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 |
| 2006-10-31 |
Enrico Zoli | Integration_algebras.ma split into 6 different files.
|
commit | commitdiff | tree |
| 2006-10-31 |
Enrico Zoli | Syntax changed (to be changed back) for left parameters...
|
commit | commitdiff | tree |
| 2006-10-24 |
Enrico Zoli | Added unit to rings.
|
commit | commitdiff | tree |
| 2006-10-24 |
Enrico Zoli | More coercions added in the algebraic hierarchy.
|
commit | commitdiff | tree |
| 2006-10-24 |
Enrico Zoli | Up to f_algebras.
|
commit | commitdiff | tree |
| 2006-10-20 |
Enrico Zoli | Up to f_algebras.
|
commit | commitdiff | tree |
| 2006-10-20 |
Enrico Zoli | 1. developed up to algebras
|
commit | commitdiff | tree |
| 2006-10-20 |
Enrico Zoli | Serious bug fixed: without a Lazy.force the user obtained...
|
commit | commitdiff | tree |
| 2006-10-16 |
Enrico Zoli | Beginning of the development of integration algebras.
|
commit | commitdiff | tree |
| 2006-10-12 |
acciavat | auto => auto new.
|
commit | commitdiff | tree |
| 2006-10-12 |
acciavat | Manual porting of CoRN to Matita.
|
commit | commitdiff | tree |
| 2006-10-03 |
maiorino | Some declarative tactics did not allow the "done" option...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | Automation enabled for declarative proofs. Cool.
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | "that is equivalent to" and "or equivalently" implemented...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | All the declarative tactics now have a more or less...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | Declarative tactics for rewriting steps, elimination...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | Notation for the existential quantifier moved to core_notati...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | New declarative commands (ast, pretty-printing and...
|
commit | commitdiff | tree |
| 2006-07-11 |
maiorino | First experimental version of the declarative proof...
|
commit | commitdiff | tree |
| 2006-03-10 |
marangon | Added inversion principle creation for inductive predicates.
|
commit | commitdiff | tree |
| 2006-03-10 |
marangon | Inversion code cleaning.
|
commit | commitdiff | tree |
| 2006-03-03 |
marangon | PP of Refine.RefineFailure.
|
commit | commitdiff | tree |
| 2006-01-11 |
marangon | Code clean up.
|
commit | commitdiff | tree |
| 2005-12-15 |
marangon | New tactic: inversion.
|
commit | commitdiff | tree |
| 2005-12-15 |
marangon | New tactic: inversion.
|
commit | commitdiff | tree |
| 2005-12-15 |
marangon | ...
|
commit | commitdiff | tree |
| 2005-12-15 |
marangon | added -I ../.. (for coq.ma)
|
commit | commitdiff | tree |
| 2004-03-31 |
Lionel Mamane | Meta files are in METAS subdir
|
commit | commitdiff | tree |
| 2004-03-31 |
Lionel Mamane | Install to findlib-defined dest dir, not to stdlib dir
|
commit | commitdiff | tree |
| 2004-03-12 |
acerioni | New tactic Auto.
|
commit | commitdiff | tree |
| next |
projects / helm.git / search