2010-07-27 blanchet 2010-07-27 complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
2010-07-27 blanchet 2010-07-27 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
2010-07-27 blanchet 2010-07-27 implemented "sublinear" minimization algorithm
2010-07-27 blanchet 2010-07-27 shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
2010-07-26 blanchet 2010-07-26 prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
2010-07-26 blanchet 2010-07-26 remove obsolete field in record
2010-07-26 blanchet 2010-07-26 simplify code
2010-07-26 blanchet 2010-07-26 get rid of obsolete "axiom ID" component, since it's now always 0
2010-07-26 blanchet 2010-07-26 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
2010-07-26 blanchet 2010-07-26 added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
2010-07-26 blanchet 2010-07-26 simplify code
2010-07-26 blanchet 2010-07-26 kill Skolem handling in Sledgehammer
2010-07-26 blanchet 2010-07-26 simplify "conjecture_shape" business, as a result of using FOF instead of CNF
2010-07-26 blanchet 2010-07-26 generate full first-order formulas (FOF) in Sledgehammer
2010-07-26 blanchet 2010-07-26 make TPTP generator accept full first-order formulas
2010-07-26 blanchet 2010-07-26 reorder SPASS conjectures correctly, based on Flotter output
2010-07-23 blanchet 2010-07-23 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; this is rather involved because the Flotter FOF-to-CNF translator is normally implicit. We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.
2010-07-21 blanchet 2010-07-21 renamings + only need second component of name pool to reconstruct proofs
2010-07-21 blanchet 2010-07-21 rename "classrel" to "class_rel"
2010-07-21 blanchet 2010-07-21 renamed "Literal" to "FOLLiteral"
2010-07-21 blanchet 2010-07-21 renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators
2010-06-30 blanchet 2010-06-30 rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly
2010-06-29 blanchet 2010-06-29 Sledgehammer can save some msecs by cheating
2010-06-29 blanchet 2010-06-29 more precise error message for remote ATPs
2010-06-29 blanchet 2010-06-29 rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
2010-06-29 blanchet 2010-06-29 move functions not needed by Metis out of "Metis_Clauses"
2010-06-28 blanchet 2010-06-28 adapt call
2010-06-25 blanchet 2010-06-25 got rid of "respect_no_atp" option, which even I don't use
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
2010-06-25 blanchet 2010-06-25 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)
2010-06-25 blanchet 2010-06-25 split SPASS time slot between SOS and non-SOS, in case SOS times out
2010-06-23 blanchet 2010-06-23 if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
2010-06-22 blanchet 2010-06-22 factor out TPTP format output into file of its own, to facilitate further changes
2010-06-22 blanchet 2010-06-22 missing "Unsynchronized" + make exception take a unit
2010-06-22 blanchet 2010-06-22 merge "generic_prover" and "generic_tptp_prover"
2010-06-22 blanchet 2010-06-22 removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
2010-06-21 blanchet 2010-06-21 thread "full_types"
2010-06-14 blanchet 2010-06-14 better error reporting for Vampire
2010-06-14 blanchet 2010-06-14 expect SPASS 3.7, and give a friendly warning if an older version is used
2010-06-14 blanchet 2010-06-14 improve ATP-specific error messages
2010-06-05 blanchet 2010-06-05 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
2010-06-05 blanchet 2010-06-05 fix remote Vampire diagnosis
2010-06-04 blanchet 2010-06-04 recongize one more outcome string for "remote_vampire"
2010-05-28 blanchet 2010-05-28 make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-17 blanchet 2010-05-17 identify common SPASS error more clearly
2010-05-14 blanchet 2010-05-14 renamed options
2010-05-14 blanchet 2010-05-14 renamed two Sledgehammer options
2010-05-14 blanchet 2010-05-14 query _HOME environment variables at run-time, not at build-time
2010-05-14 blanchet 2010-05-14 pass "full_type" argument to proof reconstruction
2010-04-29 blanchet 2010-04-29 in "overlord" mode: ignore problem prefix specified in the .thy file
2010-04-28 blanchet 2010-04-28 back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
2010-04-28 blanchet 2010-04-28 properly extract SPASS proof
2010-04-28 blanchet 2010-04-28 try out Vampire 11 and parse its output correctly; will revert to Vampire 9 if 11 doesn't perform as well
2010-04-28 blanchet 2010-04-28 removed "sorts" option, continued
2010-04-27 blanchet 2010-04-27 tuning
2010-04-27 blanchet 2010-04-27 remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
2010-04-26 blanchet 2010-04-26 rename options and keep track of conjecture shape (to facilitate proof reconstruction)
2010-04-25 blanchet 2010-04-25 support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-23 blanchet 2010-04-23 cosmetics