tuning

fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs

use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...

beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)

minor doc fixes

adapt to new type system names

restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"

take "partial_types" option with a grain of salt

fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings

close formula universally, to make SPASS happy

fixed embarrassing bug where conjecture and fact offsets were swapped

pick up GaveUp error on SystemOnTPTP

avoid trailing digits for SNARK (type) names -- grr...

document new type system syntax

use ! for mildly unsound and !! for very unsound encodings

use new type system syntax

implement the new ATP type system in Sledgehammer

define type system in ATP module so that ATPs can suggest a type system

made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support

merge symbol declarations that are type-instances of each other -- useful for type system "Args true" with monomorphization turned off

drop even more bound types in symbol declarations -- useful in particular for type system "Args true"

tuning

got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly

drop "fequal" type args for unmangled type systems

recognize more SystemOnTPTP errors

cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0

make sure that fequal keeps its type arguments for mangled type systems

no needless "fequal" proxies if "explicit_apply" is set + always have readable names

shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs

avoid Type.TYPE_MATCH exception for "True_or_False" for "If"

proper handling of partially applied proxy symbols

make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type

improve helper type instantiation code

killed needless datatype "combtyp" in Metis

have properly type-instantiated helper facts (combinators and If)

don't destroy sym table entry for special symbols such as "hAPP" if "explicit_apply" is set

better known failure recognition for ToFoF-E

cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation

fixed min-arity computation when "explicit_apply" is specified

fixed "tags" type encoding after latest round of changes

more higher-order tests for Sledgehammer/ATP

added friendly hint when Isar proof is missing

fix handling of proxies after recent drastic changes to the type encodings

added a hint to Metis errors suggesting metisFT -- it sometimes work

reconstruct TFF type predicates correctly for ToFoF

fixed parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y))

handle special constants correctly in Isar proof reconstruction code, especially type predicates

make sure the minimizer monomorphizes when it should

fixed arity of special constants if "explicit_apply" is set

make sure typing fact names are unique (needed e.g. by SNARK)

minor cleanup

reimplemented the hAPP introduction code so that it's done earlier, when the types are still available

declare TFF types so that SNARK can be used with types

perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it

move type declarations to the front, for TFF-compliance

use postfix syntax for mangled types, for consistency with unmangled