| Tue, 23 Nov 2010 18:26:56 +0100 |
blanchet |
added "verbose" option to Metis to shut up its warnings if necessary
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
fixed order of quantifier instantiation in new Skolemizer
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
more work on new Skolemizer without Hilbert_Choice
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
make handling of parameters more robust, by querying the goal
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 16:32:13 +0200 |
blanchet |
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:11:23 +0200 |
blanchet |
clearer error messages
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 18:02:14 +0700 |
blanchet |
added "trace_metis" configuration option, replacing old-fashioned references
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 17:56:41 +0200 |
blanchet |
move code from "Metis_Tactics" to "Metis_Reconstruct"
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 12:50:45 +0200 |
blanchet |
tuned comments
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:45:10 +0200 |
blanchet |
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
| base
|