]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_paramodulation/paramod.mli
milestone in basic_2, λδ-2A reconstructed
[helm.git] / helm / software / components / ng_paramodulation / paramod.mli
2010-03-18 Andrea AspertiExporting the demodulation function.
2010-01-11 Andrea Asperti1. New paramodulation function
2009-12-18 Andrea AspertiFinal subst returned by superposition and passed around.
2009-12-02 Andrea AspertiPassive equations have their own index (not passive...
2009-11-25 Andrea AspertiExported forward_inference_step
2009-07-20 Wilmer Ricciottiadded a flag for age selection
2009-07-13 Enrico Tassimatitaprover is now flexible enough to allow the comput...
2009-07-09 Enrico TassiNew functorialization: paramod is abstracted over a...
2009-07-02 Enrico Tassireturn type of paramod fixed according to the SZSOntology
2009-06-25 Enrico Tassitimeouts are passed as arguments, so that tptpprover can
2009-06-25 Enrico Tassithe prover is almost OK, types in fuctors a bit extended to
2009-06-25 Enrico Tassicode refactoring for paramodulation
2009-06-18 denesFixed wrong types in proof terms
2009-06-17 Claudio Sacerdoti... Initial implementation of statuses using objects in...
2009-06-16 Enrico Tassifirst proof reconstruction attempt, still bugged since it
2009-06-11 denesActive goals are now demodulated after selecting a...
2009-06-09 Enrico Tassisnaphost: supright almost done
2009-06-05 denesFirst tests for paramodulation (pretty printer, unifica...