| 2005-12-05 |
Alberto Griggio | added function term_of_equality to re-build the Cic...
|
commit | commitdiff | tree |
| 2005-12-05 |
Alberto Griggio | removed original equalities from the output of main_demod_eq...
|
commit | commitdiff | tree |
| 2005-12-05 |
Alberto Griggio | removed some debug messages
|
commit | commitdiff | tree |
| 2005-12-05 |
Alberto Griggio | added function saturate_equations that tries to infer...
|
commit | commitdiff | tree |
| 2005-10-17 |
Alberto Griggio | added some comments; general code cleanup
|
commit | commitdiff | tree |
| 2005-10-12 |
Alberto Griggio | fixed a couple of bugs that broke tests...
|
commit | commitdiff | tree |
| 2005-10-11 |
Alberto Griggio | fixed bugs in Indexing.find_matches and Saturation...
|
commit | commitdiff | tree |
| 2005-10-10 |
Alberto Griggio | fixed a bug (status not reset properly between calls...
|
commit | commitdiff | tree |
| 2005-09-29 |
Alberto Griggio | non-default equalities in equations_for_goal
|
commit | commitdiff | tree |
| 2005-09-29 |
Alberto Griggio | upgraded code to work with non-default equalities
|
commit | commitdiff | tree |
| 2005-09-26 |
Alberto Griggio | new signature of auto_tac, with a new optional argument...
|
commit | commitdiff | tree |
| 2005-09-26 |
Alberto Griggio | new paramodulation
|
commit | commitdiff | tree |
| 2005-09-26 |
Alberto Griggio | *** empty log message ***
|
commit | commitdiff | tree |
| 2005-09-26 |
Alberto Griggio | new signature of auto_tac, with a new optional argument...
|
commit | commitdiff | tree |
| 2005-09-26 |
Alberto Griggio | added apply_tac_verbose_with_subst, returning a Cic...
|
commit | commitdiff | tree |
| 2005-09-21 |
Alberto Griggio | bugfix on proof construction
|
commit | commitdiff | tree |
| 2005-09-06 |
Alberto Griggio | added dirty hack to blacklist mult_n_2, which causes...
|
commit | commitdiff | tree |
| 2005-09-01 |
Alberto Griggio | changed default parameter values...
|
commit | commitdiff | tree |
| 2005-08-31 |
Alberto Griggio | fixed bug in compute_equality_weight caused by wrong...
|
commit | commitdiff | tree |
| 2005-08-22 |
Alberto Griggio | some fixes
|
commit | commitdiff | tree |
| 2005-08-05 |
Alberto Griggio | some bugs fixed
|
commit | commitdiff | tree |
| 2005-08-01 |
Alberto Griggio | fixed compilation warnings
|
commit | commitdiff | tree |
| 2005-07-22 |
Alberto Griggio | added optional "paramodulation" parameter to auto to...
|
commit | commitdiff | tree |
| 2005-07-22 |
Alberto Griggio | added optional "paramodulation" parameter to auto to...
|
commit | commitdiff | tree |
| 2005-07-22 |
Alberto Griggio | - better exception handling
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | added some typechecks to avoid using equations with...
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | dependencies
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | removed .depend from .cvsignore
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | added some typechecks to avoid using equations with...
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | added CicNotation.load_notation call to disambiguate...
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | if paramodulation fails, go on with the normal auto...
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | removed old broken code
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | integration with paramodulation
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | integration with paramodulation
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | modifications/fixes for the integration with auto
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | entry point of the stand-alone saturate
|
commit | commitdiff | tree |
| 2005-07-21 |
Alberto Griggio | added paramodulation package
|
commit | commitdiff | tree |
| 2005-07-18 |
Alberto Griggio | adding library support (not ready yet)
|
commit | commitdiff | tree |
| 2005-07-11 |
Alberto Griggio | now proofs have the correct type :-)
|
commit | commitdiff | tree |
| 2005-07-01 |
Alberto Griggio | fixed bug in proof generation, new weight function...
|
commit | commitdiff | tree |
| 2005-07-01 |
Alberto Griggio | removed first Cic.term from type equality, added an...
|
commit | commitdiff | tree |
| 2005-06-30 |
Alberto Griggio | proofs are now built lazily at the end of the computation
|
commit | commitdiff | tree |
| 2005-06-29 |
Alberto Griggio | various updates, removed proofs for now because they...
|
commit | commitdiff | tree |
| 2005-06-23 |
Alberto Griggio | added various profiling statistics...
|
commit | commitdiff | tree |
| 2005-06-22 |
Alberto Griggio | reverted to previous version, as it worked better...
|
commit | commitdiff | tree |
| 2005-06-22 |
Alberto Griggio | use of discrimination trees instead of path indexes...
|
commit | commitdiff | tree |
| 2005-06-22 |
Alberto Griggio | trie structure implementation
|
commit | commitdiff | tree |
| 2005-06-20 |
Alberto Griggio | some optimizations...
|
commit | commitdiff | tree |
| 2005-06-20 |
Alberto Griggio | testing...
|
commit | commitdiff | tree |
| 2005-06-20 |
Alberto Griggio | *** empty log message ***
|
commit | commitdiff | tree |
| 2005-06-20 |
Alberto Griggio | discrimination trees
|
commit | commitdiff | tree |
| 2005-06-19 |
Alberto Griggio | limited-resource-strategy implementation (now working!)
|
commit | commitdiff | tree |
| 2005-06-19 |
Alberto Griggio | path indexing integration, limited-resource-strategy...
|
commit | commitdiff | tree |
| 2005-06-19 |
Alberto Griggio | path indexing integration
|
commit | commitdiff | tree |
| 2005-06-19 |
Alberto Griggio | path indexing working!
|
commit | commitdiff | tree |
| 2005-06-17 |
Alberto Griggio | profiling experiments...
|
commit | commitdiff | tree |
| 2005-06-15 |
Alberto Griggio | now something works...
|
commit | commitdiff | tree |
| 2005-06-10 |
Alberto Griggio | integrated indexing.ml, breaks everything :-P (previous...
|
commit | commitdiff | tree |
| 2005-06-09 |
Alberto Griggio | prima implementazione di demodulate, superposition_left...
|
commit | commitdiff | tree |
| 2005-06-09 |
Alberto Griggio | cambiato il tipo equality, aggiunto l'ordinamento tra...
|
commit | commitdiff | tree |
| 2005-06-07 |
Alberto Griggio | *** empty log message ***
|
commit | commitdiff | tree |
| 2005-05-19 |
Alberto Griggio | added lpo term-ordering
|
commit | commitdiff | tree |
| 2005-05-19 |
Alberto Griggio | various optimizations (to paramodulation and passive...
|
commit | commitdiff | tree |
| 2005-05-15 |
Alberto Griggio | added saturation.opt to the ignore list
|
commit | commitdiff | tree |
| 2005-05-15 |
Alberto Griggio | fixes (mainly) to demodulation and meta_convertibility
|
commit | commitdiff | tree |
| 2005-05-13 |
Alberto Griggio | exported new_metasenv_for_apply, needed by the paramodulatio...
|
commit | commitdiff | tree |
| 2005-05-13 |
Alberto Griggio | fixed demodulation bug
|
commit | commitdiff | tree |
| 2005-05-13 |
Alberto Griggio | moved string_of_equality into utils
|
commit | commitdiff | tree |
| 2005-05-12 |
Alberto Griggio | first commit of paramodulation-based theorem proving...
|
commit | commitdiff | tree |
|
projects / helm.git / search