]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_paramodulation
added config.ac to the tarball for debian packages
[helm.git] / helm / software / components / ng_paramodulation /
2015-01-22 Ferruccio Guididependences update
2010-10-17 Enrico Tassifixed List.for_all2 called without knowing if the two...
2010-04-19 Andrea Aspertialpha_eq instead of pervasives.compare
2010-04-13 Enrico Tassisame heads different arity -> INCOMPARABLE
2010-03-25 Andrea AspertiExtension of demod to arbtrary predicates (not just...
2010-03-24 Claudio Sacerdoti... Axioms were not indexed.
2010-03-24 Claudio Sacerdoti... ...
2010-03-23 Andrea AspertiFixed a few bugs
2010-03-23 Andrea Asperti"flat" function (subst unfolding)
2010-03-18 Andrea AspertiDebugging disabled.
2010-03-18 Andrea AspertiExporting the demodulation function.
2010-03-16 Claudio Sacerdoti... Comparison of two applications with a different number...
2010-03-04 Andrea AspertiSmall changes for debugging
2010-03-04 Andrea AspertiFixed a bug in deep_eq: we generated new clauses but...
2010-03-04 Andrea AspertiCorrected a bug relative to the application of substs...
2010-02-19 Andrea AspertiAdded an implicit parameter to branch_tac to allow...
2010-02-08 Andrea AspertiSome changes towards integration of setoid-rewriting.
2010-02-03 Claudio Sacerdoti... Debug code commented out.
2010-01-27 Andrea AspertiUnfolded exact letins during proof reconstruction.
2010-01-18 Andrea AspertiKeeping Implicit for refinement (instead of transformin...
2010-01-11 Andrea Asperti1. New paramodulation function
2010-01-11 Andrea Aspertisaturate cust be called with delta=0
2010-01-11 Andrea AspertiAdded is_equation
2010-01-11 Andrea AspertiDebugging info
2010-01-08 Andrea AspertiThe body of constants is a reference, not the actual...
2010-01-08 Andrea Aspertiremoved debugging info
2010-01-08 Andrea Aspertinew reloc_subst (to avoid cyclic substitutions).
2009-12-21 Andrea AspertiTrying to be faster
2009-12-18 Andrea AspertiFinal subst returned by superposition and passed around.
2009-12-18 Andrea Aspertiusing = instead of alpha conversions. context metasenv...
2009-12-09 Andrea AspertiDebug set to ()
2009-12-09 Andrea AspertiClean up of debgging info
2009-12-09 Andrea AspertiSyntax error
2009-12-09 Andrea AspertiWrong reference corrected
2009-12-09 Andrea AspertiMinor fixing for last chance
2009-12-09 Andrea AspertiAdded a fol operation
2009-12-02 Andrea AspertiThe new paramodulation functions instantiated over...
2009-12-02 Andrea AspertiNew ways for initialising the signature required for...
2009-12-02 Andrea AspertiPassive equations have their own index (not passive...
2009-12-02 Andrea Aspertidebug takes lazy strings. Moved here the are_alpha_eq...
2009-12-02 Andrea AspertiAdded a function remove_unit_clause
2009-12-02 Andrea AspertiAdded a boolean test function to discriminate equations...
2009-12-02 Andrea AspertiGeneralized intitialization for EqP
2009-12-02 Andrea AspertiGeneralized initialization of eqP.
2009-11-25 Andrea AspertiExported forward_inference_step
2009-11-23 Andrea AspertiRemoved dead code
2009-11-16 Wilmer RicciottiImplementation of ndestruct tactic (including destructi...
2009-10-22 Enrico Tassinew instantiate, only known bug is w.r.t. in/out scope...
2009-10-07 Claudio Sacerdoti... - oCic2NCic and nCic2OCic moved to ng_library
2009-10-06 Wilmer RicciottiInverters/Inversion:
2009-10-05 Enrico Tassiadded auto_cache in the dupable status after an
2009-10-02 Wilmer RicciottiUpdated command ninverter. Syntax:
2009-10-02 Claudio Sacerdoti... ...
2009-09-30 Wilmer RicciottiAdded initial support for inversion principles in Matit...
2009-09-21 Enrico Tassihuge commit regarding universes:
2009-09-09 Enrico Tassidepends
2009-09-09 Enrico Tassisome more work for ng-coercions
2009-07-29 Andrea AspertiNew demodulation (innermost, optimized to avoid reducin...
2009-07-29 Andrea AspertiChanged the ordering of rels, and the introduction...
2009-07-29 Andrea AspertiLazy strings
2009-07-27 denesRemoved meaningless time information
2009-07-22 denesFixed test for invertibility
2009-07-22 denesNow using lazy strings for debug printings
2009-07-21 denesImplemented handling of Invertible equalities
2009-07-20 Enrico Tassisorted modules
2009-07-20 Wilmer Ricciottiadded a flag for age selection
2009-07-20 denesOne-side indexing for commutativity
2009-07-20 denesNo demod call on functionnal symbols
2009-07-16 denesDisabled age selection and ad hoc goal weight computation
2009-07-15 Wilmer RicciottiFixed dependency function, which was lacking the code...
2009-07-14 denes.
2009-07-14 denes.
2009-07-13 Enrico Tassistatistics are used, when possible, to sort
2009-07-13 denesAdded statistics module
2009-07-13 Enrico Tassimatitaprover is now flexible enough to allow the comput...
2009-07-10 denesRemoved unused parameter of unification procedure ...
2009-07-10 Enrico Tassimore profilers
2009-07-09 Enrico TassiNew functorialization: paramod is abstracted over a...
2009-07-09 denesFixed check for condition iv p.33 (Riazzanov)
2009-07-09 Enrico Tassiprofile most operations, do not return a filtered varli...
2009-07-09 Enrico Tassitwo cases should be assert false at least in TPTP
2009-07-09 Enrico Tassimicro optimizations to unification
2009-07-09 denesCleaned a bit
2009-07-09 Enrico Tassiactivate kbo, not lpo
2009-07-07 Claudio Sacerdoti... 1) Include files for NG were neither recursively proces...
2009-07-06 denesTried to implement lpo in a more efficient way
2009-07-06 denesFixed typo in lpo (from old implementation)
2009-07-03 denesPorted old implementation of LPO (for test purposes)
2009-07-03 denesImplemented LPO
2009-07-02 denesNew age selection
2009-07-02 Enrico Tassireturn type of paramod fixed according to the SZSOntology
2009-06-30 denesMoved ID management inside the bag
2009-06-30 denesEnabled age selection (ratio 1/5)
2009-06-29 Enrico Tassi...
2009-06-29 Enrico Tassido not infer on closed goals
2009-06-29 denesFirst attempt for refined goal selection strategy
2009-06-29 Enrico Tassiadded (but not active) last chance idea
2009-06-29 denesImplemented orphan murdering technique
2009-06-26 Andrea Aspertiattempt to run a last chance procedure after the timeout
2009-06-26 Andrea Aspertithis case is not assert false since it can happen if...
next