isabelle: Graph

pass props not thms to ATP translator
2011-06-07, by blanchet
slighly more reasonable Vampire slices (until new monomorphizer is used)
2011-06-06, by blanchet
removed confusing slicing logic
2011-06-06, by blanchet
suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
2011-06-06, by blanchet
effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
2011-06-06, by blanchet
minor: curly brackets, not square brackets
2011-06-06, by blanchet
document metis better in Sledgehammer docs
2011-06-06, by blanchet
updated Sledgehammer message
2011-06-06, by blanchet
removed old optimization that isn't one anyone
2011-06-06, by blanchet
generate less type information in polymorphic case
2011-06-06, by blanchet
Metis code cleanup
2011-06-06, by blanchet
enable new Metis
2011-06-06, by blanchet
made "explicit_apply"'s smart mode (more) complete
2011-06-06, by blanchet
fall back in case path finder fails -- these errors are sometimes salvageable
2011-06-06, by blanchet
compile
2011-06-06, by blanchet
change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"
2011-06-06, by blanchet
marked "metisF" as legacy -- nobody uses it or needs it
2011-06-06, by blanchet
more preparations towards hijacking Metis
2011-06-06, by blanchet
remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
2011-06-06, by blanchet
don't mention "metisX" so much in the docs -- it will go away soon
2011-06-06, by blanchet
reintroduced metisFT in example
2011-06-06, by blanchet
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
2011-06-06, by blanchet
imported patch metis_reconstr_give_type_infer_a_chance
2011-06-06, by blanchet
make "metisX"'s default more like old "metis"
2011-06-06, by blanchet
whitespace tuning
2011-06-06, by blanchet
tuned Metis examples
2011-06-06, by blanchet
more through tests of new Metis
2011-06-06, by blanchet
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
2011-06-06, by blanchet
fixed type helper indices in new Metis
2011-06-06, by blanchet
improved ATP clausifier so it can deal with "x => (y <=> z)"
2011-06-06, by blanchet
avoid renumbering hypotheses
2011-06-06, by blanchet
fixed reconstruction of new Skolem constants in new Metis
2011-06-06, by blanchet
don't translate new Skolemizer assumptions in new Metis
2011-06-06, by blanchet
tuning
2011-06-06, by blanchet
fixed detection of Skolem constants in type construction detection code
2011-06-06, by blanchet
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
2011-06-06, by blanchet
tuning
2011-06-06, by blanchet
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
2011-06-06, by blanchet
reveal Skolems in new Metis
2011-06-06, by blanchet
don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
2011-06-06, by blanchet
slacker version of "fastype_of", in case a function has dummy type
2011-06-06, by blanchet
don't stumble on Skolem names
2011-06-06, by blanchet
conceal old Skolems in new Metis
2011-06-06, by blanchet
don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs
2011-06-06, by blanchet
use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
2011-06-06, by blanchet
properly unmangle names in path finder
2011-06-06, by blanchet
only uncombine combinators in textual Isar proofs, not in Metis
2011-06-06, by blanchet
properly locate helpers whose constants have several entries in the helper table
2011-06-06, by blanchet
skip "hBOOL" in new Metis path finder
2011-06-06, by blanchet
don't pass "~ " to new Metis
2011-06-06, by blanchet
tuning
2011-06-06, by blanchet
gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings
2011-06-06, by blanchet
temporarily document "metisX"
2011-06-06, by blanchet
use "metisX" as fallback, since it's much faster than "metisFT"
2011-06-06, by blanchet
temporarily added "MetisX" as reconstructor and minimizer
2011-06-06, by blanchet
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
2011-06-06, by blanchet
show what failed to play
2011-06-06, by blanchet
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
2011-06-06, by blanchet
tuning
2011-06-06, by blanchet
killed odd connectives
2011-06-06, by blanchet
added Metis examples to test the new type encodings
2011-06-06, by blanchet
tuned CASC method
2011-06-06, by blanchet
clean up unnecessary machinery -- helpers work also with monomorphic type encodings
2011-06-06, by blanchet
added support for helpers in new Metis, so far only for polymorphic type encodings
2011-06-06, by blanchet
imported rest of new IMP
2011-06-06, by kleing
atLeastAtMostSuc_conv on int
2011-06-06, by kleing
fixed typo
2011-06-06, by kleing
updated SMT certificates
2011-06-05, by boehmes
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
2011-06-05, by boehmes
changing the mira setting again for the mutabelle configuration
2011-06-03, by bulwahn
adding more settings to mira's mutabelle configuration
2011-06-03, by bulwahn
merged
2011-06-02, by nipkow
Added typed IMP
2011-06-02, by nipkow
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
2011-06-02, by bulwahn
adding invocation of exhaustive testing without using finite types to mutabelle
2011-06-02, by bulwahn
moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle
2011-06-02, by bulwahn
splitting Dlist theory in Dlist and Dlist_Cset
2011-06-02, by bulwahn
merged
2011-06-01, by nipkow
Made comments text
2011-06-01, by nipkow
Fixed denotational semantics
2011-06-01, by nipkow
Removed old IMP files
2011-06-01, by nipkow
Replacing old IMP with new Semantics material
2011-06-01, by nipkow
tuned lemmas
2011-06-01, by nipkow
fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
2011-06-01, by blanchet
setting up code generation for extended reals
2011-06-01, by bulwahn
new lemmas
2011-06-01, by nipkow
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
2011-06-01, by blanchet
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
2011-06-01, by blanchet
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
2011-06-01, by blanchet
fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume"
2011-06-01, by blanchet
ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
2011-06-01, by blanchet
fixed interaction between type tags and hAPP in reconstruction code
2011-06-01, by blanchet
implemented missing hAPP and ti cases of new path finder
2011-06-01, by blanchet
support lightweight tags in new Metis
2011-06-01, by blanchet
tuned names
2011-06-01, by blanchet
export one more function
2011-06-01, by blanchet
clausify "<=>" (needed for some type information)
2011-06-01, by blanchet
distinguish different kinds of typing informations in the fact name
2011-06-01, by blanchet
splitting RBT theory into RBT and RBT_Mapping
2011-06-01, by bulwahn
creating a free variable with proper name and local mixfix syntax (cf. db9b9e46131c)
2011-06-01, by bulwahn
code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps
2011-06-01, by bulwahn
make SML/NJ happier
2011-06-01, by blanchet
make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
2011-06-01, by blanchet
speed up example by disabling preplay, and temporarily comment out a broken Sledgehammer call
2011-05-31, by blanchet
updated SMT certificates
2011-05-31, by boehmes
proper nesting of loops in new monomorphizer;
2011-05-31, by boehmes
use new monomorphizer for SMT;
2011-05-31, by boehmes
merged
2011-05-31, by bulwahn
Quickcheck Narrowing only requires one compilation with GHC now
2011-05-31, by bulwahn
splitting test_goal_terms in Quickcheck into smaller basic functions
2011-05-31, by bulwahn
adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
2011-05-31, by bulwahn
compile
2011-05-31, by blanchet
compile
2011-05-31, by blanchet
monomorphize in the new Metis if the type system calls for it
2011-05-31, by blanchet
use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
2011-05-31, by blanchet
fixed comment
2011-05-31, by blanchet
fixed new path finder for type information tag
2011-05-31, by blanchet
no need for type arguments with "xxx_tags_heavy" type system
2011-05-31, by blanchet
use ":" for type information (looks good in Metis's output) and handle it in new path finder
2011-05-31, by blanchet
tuned name
2011-05-31, by blanchet
tuned name
2011-05-31, by blanchet
make "prepare_atp_problem" more robust w.r.t. choice of type system
2011-05-31, by blanchet
parse optional type system specification
2011-05-31, by blanchet
tuning
2011-05-31, by blanchet
proper handling of type variable classes in new Metis
2011-05-31, by blanchet
fixed recursive call in new path finder and (untested:) handle hAPP
2011-05-31, by blanchet
don't preprocess twice
2011-05-31, by blanchet
more robust and simpler adjustment computation
2011-05-31, by blanchet
more work on new Metis
2011-05-31, by blanchet
tuning
2011-05-31, by blanchet
more work on new metis that exploits the powerful new type encodings
2011-05-31, by blanchet
tuning
2011-05-31, by blanchet
removed obscure option
2011-05-31, by blanchet
added "metisX" syntax (temporary)
2011-05-31, by blanchet
compile
2011-05-31, by blanchet
added new metis mode, with no implementation yet
2011-05-31, by blanchet
tuning
2011-05-31, by blanchet
first step in sharing more code between ATP and Metis translation
2011-05-31, by blanchet
more precise authorship, reflecting my own ignorance and hg annotate
2011-05-31, by krauss
generate raw induction rule as instance of generic rule with careful treatment of currying
2011-05-31, by krauss
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
2011-05-31, by krauss
admissibility on option type
2011-05-31, by krauss
also manage induction rule;
2011-05-23, by krauss
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
2011-05-30, by bulwahn
merged
2011-05-30, by paulson
Workaround for bug involving makeindex, hyperref and the | symbol
2011-05-30, by paulson
parameterize print_theorems over actual search function
2011-05-30, by krauss
added experimental yxml_find_theorems web service (but no client yet)
2011-05-30, by krauss
generic ScgiServer.simple_handler
2011-05-30, by krauss
moved html templates to a separate module, making their awkward signatures explicit
2011-05-30, by krauss
attempt to clarify code; removed "handle _" and dead code
2011-05-30, by krauss
(de)serialization for search query and result
2011-05-30, by krauss
explicit type for search queries
2011-05-30, by krauss
moved questionable goal modification out of filter_theorems
2011-05-30, by krauss
exported raw query parser; removed inconsistent clone
2011-05-30, by krauss
separate query parsing from actual search
2011-05-30, by krauss
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
2011-05-30, by blanchet
document new explicit apply
2011-05-30, by blanchet
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
2011-05-30, by blanchet
don't slice if there are too few facts
2011-05-30, by blanchet
nicer failure message when one-line proof reconstruction fails
2011-05-30, by blanchet
make SML/NJ happy
2011-05-30, by blanchet
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
2011-05-30, by blanchet
make all messages urgent in verbose mode
2011-05-30, by blanchet
minimize automatically even if Metis failed, if the external prover was really fast
2011-05-30, by blanchet
fixed syntax of min options
2011-05-30, by blanchet
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
2011-05-30, by blanchet
better merging of similar outputs
2011-05-30, by blanchet
update minimization documentation
2011-05-30, by blanchet
imported patch sledge_doc_metis_as_prover
2011-05-30, by blanchet
automatically minimize with Metis when this can be done within a few seconds
2011-05-30, by blanchet
minimize with Metis if possible
2011-05-30, by blanchet
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
2011-05-30, by blanchet
Workaround for hyperref bug affecting index entries involving the | symbol
2011-05-30, by paulson
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
2011-05-30, by bulwahn
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
2011-05-30, by bulwahn
merged multiple heads
2011-05-30, by paulson
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
2011-05-30, by paulson
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
2011-05-29, by blanchet
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
2011-05-29, by blanchet
function tutorial: do not omit termination proof, even when discussing other things
2011-05-27, by krauss
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
2011-05-27, by boehmes
document new "try"
2011-05-27, by blanchet
tuned comments
2011-05-27, by blanchet
new timeout section (cf. Nitpick manual)
2011-05-27, by blanchet
cleanup proof text generation code
2011-05-27, by blanchet
more Sledgehammer documentation updates
2011-05-27, by blanchet
minor update
2011-05-27, by blanchet
try both "metis" and (on failure) "metisFT" in replay
2011-05-27, by blanchet
show time taken for reconstruction
2011-05-27, by blanchet
unbreak "max_potential" logic
2011-05-27, by blanchet
more concise output
2011-05-27, by blanchet
compile
2011-05-27, by blanchet
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
2011-05-27, by blanchet
repaired theory merging and defined/used helpers
2011-05-27, by blanchet
make Sledgehammer a little bit less verbose in "try"
2011-05-27, by blanchet
handle non-auto try cases gracefully in Try Methods
2011-05-27, by blanchet
handle non-auto try case gracefully in Solve Direct
2011-05-27, by blanchet
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
2011-05-27, by blanchet
update SML section of documentation
2011-05-27, by blanchet
handle non-auto try case gracefully in Nitpick
2011-05-27, by blanchet
handle non-auto try case of Sledgehammer better
2011-05-27, by blanchet
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-27, by blanchet
removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
2011-05-27, by blanchet
renamed "Auto_Tools" "Try"
2011-05-27, by blanchet
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
2011-05-27, by blanchet
renamed "try" "try_methods"
2011-05-27, by blanchet
renamed "metis_timeout" to "preplay_timeout" and continued implementation
2011-05-27, by blanchet
minor fixes to Sledgehammer docs
2011-05-27, by blanchet
shorten minimizer command further, exploiting until-now-undocumented syntax
2011-05-27, by blanchet
minor tweaks to the Nitpick documentation
2011-05-27, by blanchet
added syntax for specifying Metis timeout (currently used only by SMT solvers)
2011-05-27, by blanchet
readded Waldmeister as default to the documentation and other minor changes
2011-05-27, by blanchet
reintroduced Waldmeister but limit the number of remote threads created
2011-05-27, by blanchet
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
2011-05-27, by blanchet
minor doc adjustments
2011-05-27, by blanchet
make output more concise
2011-05-27, by blanchet
merge timeout messages from several ATPs into one message to avoid clutter
2011-05-27, by blanchet
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
2011-05-27, by blanchet
tuning
2011-05-27, by blanchet
mention contributions from LCP and explain metis and metisFT encodings
2011-05-27, by blanchet
fixed trivial fact detection
2011-05-27, by blanchet
cleaner handling of equality and proxies (esp. for THF)
2011-05-27, by blanchet
recognize more ATP failures
2011-05-27, by blanchet
fully support all type system encodings in typed formats (TFF, THF)
2011-05-27, by blanchet
take out Waldmeister from default for now -- success rate too low on Judgment Day
2011-05-27, by blanchet
document relevance filter a bit more
2011-05-27, by blanchet
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
2011-05-27, by blanchet
towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
2011-05-27, by blanchet
instance inat for complete_lattice
2011-05-26, by noschinl
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
2011-05-26, by boehmes
integral strong monotone; finite subadditivity for measure
2011-05-26, by hoelzl
composition of convex and measurable function is measurable
2011-05-26, by hoelzl
introduce independence of two random variables
2011-05-26, by hoelzl
add lemma indep_distribution_eq_measure
2011-05-26, by hoelzl
add lemma indep_rv_finite
2011-05-26, by hoelzl
generalize setsum_cases
2011-05-26, by hoelzl
add lemma borel_0_1_law
2011-05-26, by hoelzl
add lemma sigma_sets_singleton
2011-05-26, by hoelzl
use abbrevitation events == sets M
2011-05-26, by hoelzl