]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/paramodulation/inference.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / paramodulation / inference.mli
2005-10-25 Andrea Aspertiexperimental version
2005-10-17 Alberto Griggioadded some comments; general code cleanup
2005-10-10 Alberto Griggiofixed a bug (status not reset properly between calls...
2005-09-29 Alberto Griggioupgraded code to work with non-default equalities
2005-09-26 Alberto Griggionew paramodulation
2005-09-23 Claudio Sacerdoti... New module HMysql (to abstract over Mysql and make...
2005-09-21 Alberto Griggiobugfix on proof construction
2005-07-21 Alberto Griggiomodifications/fixes for the integration with auto
2005-07-18 Alberto Griggioadding library support (not ready yet)
2005-07-11 Alberto Griggionow proofs have the correct type :-)
2005-07-01 Alberto Griggiofixed bug in proof generation, new weight function...
2005-07-01 Alberto Griggioremoved first Cic.term from type equality, added an...
2005-06-30 Alberto Griggioproofs are now built lazily at the end of the computation
2005-06-29 Alberto Griggiovarious updates, removed proofs for now because they...
2005-06-20 Alberto Griggiosome optimizations...
2005-06-09 Alberto Griggiocambiato il tipo equality, aggiunto l'ordinamento tra...
2005-06-07 Alberto Griggio*** empty log message ***
2005-05-19 Alberto Griggiovarious optimizations (to paramodulation and passive...
2005-05-15 Alberto Griggiofixes (mainly) to demodulation and meta_convertibility
2005-05-12 Alberto Griggiofirst commit of paramodulation-based theorem proving...