User Details
User Details
- User Since
- Nov 21 2019, 6:25 PM (209 w, 6 d)
Sep 25 2023
Sep 25 2023
blanchette committed rISABELLE8ca71c0ae31f: avoid legacy binding errors in Sledgehammer Isar proofs.
avoid legacy binding errors in Sledgehammer Isar proofs
blanchette committed rISABELLEef89f1beee95: parse applie lambdas correctly plus deal gracefully with lambda-lifting in….
parse applie lambdas correctly plus deal gracefully with lambda-lifting in…
allow (~) syntax in TPTP proofs for unapplied negation
blanchette committed rISABELLE1c0576840bf4: reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs.
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
blanchette committed rISABELLE1b0f5576f5e9: use same associativity as Isabelle when parsing HOL proofs.
use same associativity as Isabelle when parsing HOL proofs
blanchette committed rISABELLE1320782a394e: improved Sledgehammer's HOL proof parser w.r.t. negation.
improved Sledgehammer's HOL proof parser w.r.t. negation
Sep 5 2023
Sep 5 2023
tuned Sledgehammer messages
respect timeout better
Aug 27 2023
Aug 27 2023
blanchette committed rISABELLE2baa77e37406: avoid using FOOL syntax with older Vampire versions because of soundness bug….
avoid using FOOL syntax with older Vampire versions because of soundness bug…
Aug 25 2023
Aug 25 2023
blanchette committed rISABELLE25f16c356dae: avoid using FOOL syntax with older Vampire versions because of soundness bug….
avoid using FOOL syntax with older Vampire versions because of soundness bug…
Jun 14 2023
Jun 14 2023
blanchette committed rISABELLEd3122089b67c: disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't….
disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't…
Apr 27 2023
Apr 27 2023
made 'primcorec' more robust
Apr 6 2023
Apr 6 2023
small simplifications
Apr 3 2023
Apr 3 2023
shortened some parts of Huffman proof using Sledgehammer
Mar 15 2023
Mar 15 2023
removed accidental junk
Mar 10 2023
Mar 10 2023
blanchette committed rISABELLE7c25451ae2c1: use simplifier to classify the missing assumptions in Sledgehammer's abduction….
use simplifier to classify the missing assumptions in Sledgehammer's abduction…
don't try to falisfy goals with schematics
Mar 8 2023
Mar 8 2023
blanchette committed rISABELLE80bcebe6cf33: require the presence of free variables to do abduction in Sledgehammer.
require the presence of free variables to do abduction in Sledgehammer
Mar 3 2023
Mar 3 2023
blanchette committed rISABELLE8a28ab58d155: detect duplicates in Sledgehammer output -- suggested by Larry Paulson.
detect duplicates in Sledgehammer output -- suggested by Larry Paulson
blanchette committed rISABELLE615a6a6a4b0b: got rid of 'important message' mechanism in SystemOnTPTP (which is less used….
got rid of 'important message' mechanism in SystemOnTPTP (which is less used…
Mar 1 2023
Mar 1 2023
tweaked Sledgehammer interaction
there won't be an E version 2.7
adopt terminology suggested by Larry Paulson
reverted 0506c3273814 -- the message is still useful
more robust E proof parsing
tweaked abduction in Sledgehammer
avoid double 'Warning:' in Sledgehammer messages
slightly more documentation
renamed new Sledgehammer option
updated documentation
improve ad hoc abduction in Sledgehammer
implemented ad hoc abduction in Sledgehammer with E
blanchette committed rISABELLEa15f0fcff041: don't apply abduction and consistency checking to goals of the form 'False'.
don't apply abduction and consistency checking to goals of the form 'False'
Feb 20 2023
Feb 20 2023
tuned metis call to avoid obscure feature
Feb 15 2023
Feb 15 2023
removed rarely used error in Sledgehammer
blanchette committed rISABELLEbc43f86c9598: added refute mode to Sledgehammer to find 'counterexamples'.
added refute mode to Sledgehammer to find 'counterexamples'
Feb 13 2023
Feb 13 2023
blanchette committed rISABELLE27be31d7ad88: careful eta-contraction in Metis to keep argument to All and Ex expanded.
careful eta-contraction in Metis to keep argument to All and Ex expanded
Dec 20 2022
Dec 20 2022
added lifting_forget as suggested by Peter Lammich
adapted to Isabelle/c48fe2be847f
Nov 23 2022
Nov 23 2022
blanchette committed rISABELLE87217c655984: correctly show '(> 2 s, timed out)' or similar in Sledgehammer's output.
correctly show '(> 2 s, timed out)' or similar in Sledgehammer's output
Nov 10 2022
Nov 10 2022
use timeout with MiniSat
Oct 17 2022
Oct 17 2022
blanchette committed rISABELLE73b120e0dbfe: generate some metainformation not only for SPASS but also for Zipperposition….
generate some metainformation not only for SPASS but also for Zipperposition…
Sep 5 2022
Sep 5 2022
blanchette committed rISABELLE6a20d0ebd5b3: added a bound in SMT on the number of schematic constants considered -- the….
added a bound in SMT on the number of schematic constants considered -- the…
Sep 2 2022
Sep 2 2022
replaced slow smt call by blast
Aug 25 2022
Aug 25 2022
Aug 18 2022
Aug 18 2022
reintroduced SPASS to the mix
Aug 17 2022
Aug 17 2022
tweaked generation of Isar proofs
blanchette committed rISABELLE8bfad7bc74cb: tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and….
tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and…
Aug 16 2022
Aug 16 2022
revived 'try0' and 'smart' Isar proofs in Sledgehammer
Aug 12 2022
Aug 12 2022
blanchette committed rISABELLE2b106aae897c: added support for cvc5 (whose interface is almost identical to CVC4).
added support for cvc5 (whose interface is almost identical to CVC4)
Aug 5 2022
Aug 5 2022
Aug 4 2022
Aug 4 2022
more politically correct
Aug 3 2022
Aug 3 2022
added two lemmas to relational chains
Aug 2 2022
Aug 2 2022
blanchette committed rISABELLE3557f826362c: changed the order of Zipperposition slices in Sledgehammer.
changed the order of Zipperposition slices in Sledgehammer
changed confusing assumption name
Jul 29 2022
Jul 29 2022
blanchette committed rAFP9663b335a71e: removed a spurious locale parameter -- the same issue probably arises in the….
removed a spurious locale parameter -- the same issue probably arises in the…
removed needless assumption
Jul 27 2022
Jul 27 2022
added lemma about lazy list chains
Jul 26 2022
Jul 26 2022
Jul 11 2022
Jul 11 2022
prefer non-JNI SAT solvers by default in Nitpick
milder Sledgehammer messages
Apr 13 2022
Apr 13 2022
pass new option only to new version of E
Apr 8 2022
Apr 8 2022
enable an E option suggested by Petar Vukmirovic
Apr 1 2022
Apr 1 2022
blanchette committed rISABELLE840256534f34: tuned slices to get the fifth Zipperposition slice in a typical run.
tuned slices to get the fifth Zipperposition slice in a typical run
Mar 31 2022
Mar 31 2022
further tweaked E's setup
Mar 29 2022
Mar 29 2022
Mar 25 2022
Mar 25 2022
compile TPTP module
further modernized E setup
cleaned up obsolete E setup and a bit of SPASS
blanchette committed rISABELLEe1aa703c8cce: second and last step in making time slicing more flexible in Sledgehammer: try….
second and last step in making time slicing more flexible in Sledgehammer: try…
blanchette committed rISABELLEd9bb81999d2c: first step in making time slicing more flexible in Sledgehammer: label slices….
first step in making time slicing more flexible in Sledgehammer: label slices…
blanchette committed rISABELLE28d2cb99b37f: added parentheses in TPTP output -- seem necessary for some provers.
added parentheses in TPTP output -- seem necessary for some provers
Feb 22 2022
Feb 22 2022
have Sledgehammer honor 'smt_nat_as_int' option
blanchette committed rISABELLE66eb6fdfc244: handle Zipperposition definitions in Isar proof construction.
handle Zipperposition definitions in Isar proof construction
blanchette committed rISABELLEf12539c8de0c: more handling of Zipperposition definitions in Isar proof construction.
more handling of Zipperposition definitions in Isar proof construction
parse Zipperposition definitions
Feb 14 2022
Feb 14 2022
print outcome of Sledgehammer search in panel
print Sledgehammer error message
Feb 9 2022
Feb 9 2022
blanchette committed rISABELLE7cadf5a7ed5b: more liberal parsing of Sledgehammer options to allow empty lists (as suggested….
more liberal parsing of Sledgehammer options to allow empty lists (as suggested…
Feb 8 2022
Feb 8 2022
more robust TSTP proof parsing
added possibility of extra options to SMT slices
Feb 2 2022
Feb 2 2022
blanchette committed rISABELLE789e0e1a9e33: more precise slicing computation and output when not enough lemmas are….
more precise slicing computation and output when not enough lemmas are…
enable induction in one of Zipperposition's slices
blanchette committed rISABELLE14e27dedee10: made sorting of Vampire facts more robust in the face of names that deviate….
made sorting of Vampire facts more robust in the face of names that deviate…
blanchette committed rISABELLE79b4e711d6a2: robustly handle empty proof blocks in Isar proof output.
robustly handle empty proof blocks in Isar proof output
blanchette committed rISABELLE04a4881ff0fd: propagate right result when enough proofs have been found.
propagate right result when enough proofs have been found
don't lose error messages
blanchette committed rISABELLEc84a20e9b00f: correctly parse E proofs that assume '=' and '!=' bind more tightly than….
correctly parse E proofs that assume '=' and '!=' bind more tightly than…
blanchette committed rISABELLE95e3aade547d: don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in….
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in…