| Sun, 13 May 2012 16:31:01 +0200 |
blanchet |
eta-reduce definition-like equations for THF provers; Satallax in particular seems to love that
|
file |
diff |
annotate
|
| Sun, 13 May 2012 16:31:01 +0200 |
blanchet |
get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
|
file |
diff |
annotate
|
| Sun, 13 May 2012 16:31:01 +0200 |
blanchet |
extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps"
|
file |
diff |
annotate
|
| Thu, 10 May 2012 16:56:23 +0200 |
blanchet |
cleaner handling of bi-implication for THF output of first-order type encodings
|
file |
diff |
annotate
|
| Thu, 03 May 2012 13:17:15 +0200 |
wenzelm |
backout 9579464d00f9 to avoid odd crash of polyml-5.2.1 (according to Jasmin, this change is not essential for now);
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:36:27 +0200 |
blanchet |
avoid duplicate helpers
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 12:16:10 +0200 |
blanchet |
eta-expand unapplied equalities in THF rather than using a proxy
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 01:05:06 +0200 |
blanchet |
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 22:00:33 +0200 |
blanchet |
don't extensionalize formulas for higher-order provers -- Satallax in particular will only expand definitions of the form "constant = ..."
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 22:00:33 +0200 |
blanchet |
don't use the native choice operator if the type encoding isn't higher-order
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 22:00:33 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
handle TPTP definitions as definitions in Nitpick rather than as axioms
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
fix handling of atomizable conjectures without a top-level "Trueprop" (e.g. "x == (y::nat)")
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
fixed eta-extension of higher-order quantifiers in THF output
|
file |
diff |
annotate
|