src/HOL/Tools/ATP/atp_problem_generate.ML
Sun, 13 May 2012 16:31:01 +0200 blanchet eta-reduce definition-like equations for THF provers; Satallax in particular seems to love that
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
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"
Thu, 10 May 2012 16:56:23 +0200 blanchet cleaner handling of bi-implication for THF output of first-order type encodings
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);
Fri, 27 Apr 2012 22:36:27 +0200 blanchet avoid duplicate helpers
Fri, 27 Apr 2012 12:16:10 +0200 blanchet eta-expand unapplied equalities in THF rather than using a proxy
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
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 = ..."
Wed, 25 Apr 2012 22:00:33 +0200 blanchet don't use the native choice operator if the type encoding isn't higher-order
Wed, 25 Apr 2012 22:00:33 +0200 blanchet tuning
Tue, 24 Apr 2012 09:47:40 +0200 blanchet smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
Tue, 24 Apr 2012 09:47:40 +0200 blanchet handle TPTP definitions as definitions in Nitpick rather than as axioms
Tue, 24 Apr 2012 09:47:40 +0200 blanchet fix handling of atomizable conjectures without a top-level "Trueprop" (e.g. "x == (y::nat)")
Tue, 27 Mar 2012 16:59:13 +0300 blanchet fixed eta-extension of higher-order quantifiers in THF output
less more (0) -15 tip