Page MenuHomeIsabelle/Phabricator

blanchette (Jasmin Blanchette)
User

Projects

User Details

User Since
Nov 21 2019, 6:25 PM (209 w, 6 d)

Recent Activity

Sep 25 2023

blanchette committed rISABELLE41273636a82a: added argo.
added argo
Sep 25 2023, 5:47 PM
blanchette committed rISABELLE8ca71c0ae31f: avoid legacy binding errors in Sledgehammer Isar proofs.
avoid legacy binding errors in Sledgehammer Isar proofs
Sep 25 2023, 5:47 PM
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…
Sep 25 2023, 5:47 PM
blanchette committed rISABELLE5e995ceb7490: allow (~) syntax in TPTP proofs for unapplied negation.
allow (~) syntax in TPTP proofs for unapplied negation
Sep 25 2023, 5:47 PM
blanchette committed rISABELLE1c0576840bf4: reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs.
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
Sep 25 2023, 5:46 PM
blanchette committed rISABELLE1b0f5576f5e9: use same associativity as Isabelle when parsing HOL proofs.
use same associativity as Isabelle when parsing HOL proofs
Sep 25 2023, 5:46 PM
blanchette committed rISABELLE1320782a394e: improved Sledgehammer's HOL proof parser w.r.t. negation.
improved Sledgehammer's HOL proof parser w.r.t. negation
Sep 25 2023, 5:46 PM

Sep 5 2023

blanchette committed rISABELLEde8081bc85a0: tuned Sledgehammer messages.
tuned Sledgehammer messages
Sep 5 2023, 3:32 PM
blanchette committed rISABELLEa7bcd2af7190: respect timeout better.
respect timeout better
Sep 5 2023, 3:32 PM

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 27 2023, 7:42 PM

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…
Aug 25 2023, 11:37 AM

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…
Jun 14 2023, 3:56 PM

Apr 27 2023

blanchette committed rISABELLE64beebac04b8: made 'primcorec' more robust.
made 'primcorec' more robust
Apr 27 2023, 4:19 PM

Apr 6 2023

blanchette committed rAFPe9b183de6e0b: small simplifications.
small simplifications
Apr 6 2023, 10:02 AM

Apr 3 2023

blanchette committed rAFPb4d2083c0ac4: shortened some parts of Huffman proof using Sledgehammer.
shortened some parts of Huffman proof using Sledgehammer
Apr 3 2023, 4:56 PM

Mar 15 2023

blanchette committed rISABELLEb9e9b818d7b0: removed accidental junk.
removed accidental junk
Mar 15 2023, 3:28 PM

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…
Mar 10 2023, 3:48 PM
blanchette committed rISABELLEd39027e1c8c5: don't try to falisfy goals with schematics.
don't try to falisfy goals with schematics
Mar 10 2023, 12:12 PM

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 8 2023, 6:34 PM

Mar 3 2023

blanchette committed rISABELLE8a28ab58d155: detect duplicates in Sledgehammer output -- suggested by Larry Paulson.
detect duplicates in Sledgehammer output -- suggested by Larry Paulson
Mar 3 2023, 11:48 AM
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 3 2023, 11:48 AM

Mar 1 2023

blanchette committed rISABELLEe51aa922079a: tweaked Sledgehammer interaction.
tweaked Sledgehammer interaction
Mar 1 2023, 5:27 PM
blanchette committed rISABELLEcdf5f392ea78: there won't be an E version 2.7.
there won't be an E version 2.7
Mar 1 2023, 5:27 PM
blanchette committed rISABELLE110988ad5b4c: compile.
compile
Mar 1 2023, 5:27 PM
blanchette committed rISABELLE7c76221baecb: adopt terminology suggested by Larry Paulson.
adopt terminology suggested by Larry Paulson
Mar 1 2023, 5:27 PM
blanchette added a reverting change for rISABELLE0506c3273814: removed rarely used error in Sledgehammer: rISABELLE51dac6fcdd0e: reverted 0506c3273814 -- the message is still useful.
Mar 1 2023, 5:27 PM
blanchette committed rISABELLE51dac6fcdd0e: reverted 0506c3273814 -- the message is still useful.
reverted 0506c3273814 -- the message is still useful
Mar 1 2023, 5:27 PM
blanchette committed rISABELLE4cdefee3f97f: more robust E proof parsing.
more robust E proof parsing
Mar 1 2023, 5:27 PM
blanchette committed rISABELLEbde374587d93: tweaked abduction in Sledgehammer.
tweaked abduction in Sledgehammer
Mar 1 2023, 5:27 PM
blanchette committed rISABELLE4a6eb1b18340: avoid double 'Warning:' in Sledgehammer messages.
avoid double 'Warning:' in Sledgehammer messages
Mar 1 2023, 5:27 PM
blanchette committed rISABELLE73611eb994cf: slightly more documentation.
slightly more documentation
Mar 1 2023, 5:27 PM
blanchette committed rISABELLE779faa014564: renamed new Sledgehammer option.
renamed new Sledgehammer option
Mar 1 2023, 5:27 PM
blanchette committed rISABELLEe10f15652026: updated documentation.
updated documentation
Mar 1 2023, 5:27 PM
blanchette committed rISABELLE4e8a6354c54f: improve ad hoc abduction in Sledgehammer.
improve ad hoc abduction in Sledgehammer
Mar 1 2023, 5:27 PM
blanchette committed rISABELLEf6cb40234009: tuning.
tuning
Mar 1 2023, 5:27 PM
blanchette committed rISABELLEa8458f0df4ee: implemented ad hoc abduction in Sledgehammer with E.
implemented ad hoc abduction in Sledgehammer with E
Mar 1 2023, 5:27 PM
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'
Mar 1 2023, 5:27 PM

Feb 20 2023

blanchette committed rAFP7ff72891adea: tuned metis call to avoid obscure feature.
tuned metis call to avoid obscure feature
Feb 20 2023, 11:50 AM

Feb 15 2023

blanchette committed rISABELLE0506c3273814: removed rarely used error in Sledgehammer.
removed rarely used error in Sledgehammer
Feb 15 2023, 5:06 PM
blanchette committed rISABELLEbc43f86c9598: added refute mode to Sledgehammer to find 'counterexamples'.
added refute mode to Sledgehammer to find 'counterexamples'
Feb 15 2023, 10:57 AM

Feb 13 2023

blanchette committed rISABELLE8bec573e1fdc: updated NEWS.
updated NEWS
Feb 13 2023, 7:41 PM
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
Feb 13 2023, 7:37 PM

Dec 20 2022

blanchette committed rISABELLEc48fe2be847f: added lifting_forget as suggested by Peter Lammich.
added lifting_forget as suggested by Peter Lammich
Dec 20 2022, 6:24 PM
blanchette committed rAFPf31fa8686572: merge.
merge
Dec 20 2022, 6:22 PM
blanchette committed rAFP98654eb7841b: adapted to Isabelle/c48fe2be847f.
adapted to Isabelle/c48fe2be847f
Dec 20 2022, 6:22 PM

Nov 23 2022

blanchette committed rISABELLEeb294dd8e266: compile.
compile
Nov 23 2022, 11:49 AM
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 23 2022, 11:49 AM

Nov 10 2022

blanchette committed rISABELLE7956b822f239: use timeout with MiniSat.
use timeout with MiniSat
Nov 10 2022, 11:49 AM

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…
Oct 17 2022, 1:05 PM

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 5 2022, 1:13 PM

Sep 2 2022

blanchette committed rAFP10120a93e155: replaced slow smt call by blast.
replaced slow smt call by blast
Sep 2 2022, 3:04 PM

Aug 25 2022

blanchette committed rAFP358ee38a13a3: tuning.
tuning
Aug 25 2022, 11:23 AM

Aug 18 2022

blanchette committed rISABELLE77cbf472fcc9: reintroduced SPASS to the mix.
reintroduced SPASS to the mix
Aug 18 2022, 10:22 AM

Aug 17 2022

blanchette committed rISABELLE5f7d22354a65: tweaked generation of Isar proofs.
tweaked generation of Isar proofs
Aug 17 2022, 6:20 PM
blanchette committed rISABELLE8bfad7bc74cb: tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and….
tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and…
Aug 17 2022, 3:10 PM

Aug 16 2022

blanchette committed rISABELLEe7b04452eef3: revived 'try0' and 'smart' Isar proofs in Sledgehammer.
revived 'try0' and 'smart' Isar proofs in Sledgehammer
Aug 16 2022, 5:25 PM

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 12 2022, 3:35 PM

Aug 5 2022

blanchette committed rAFP855e895beb9c: more accurate name.
more accurate name
Aug 5 2022, 1:27 PM

Aug 4 2022

blanchette committed rAFP04bb771f4700: more politically correct.
more politically correct
Aug 4 2022, 4:31 PM

Aug 3 2022

blanchette committed rAFP1e9471f837af: added two lemmas to relational chains.
added two lemmas to relational chains
Aug 3 2022, 1:53 PM

Aug 2 2022

blanchette committed rISABELLEdcd3ef2905d6: merge.
merge
Aug 2 2022, 1:38 PM
blanchette committed rISABELLE3557f826362c: changed the order of Zipperposition slices in Sledgehammer.
changed the order of Zipperposition slices in Sledgehammer
Aug 2 2022, 1:38 PM
blanchette committed rAFPf78309f3fd50: changed confusing assumption name.
changed confusing assumption name
Aug 2 2022, 11:00 AM

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…
Jul 29 2022, 2:26 PM
blanchette committed rAFP8f58103dc2d4: removed needless assumption.
removed needless assumption
Jul 29 2022, 10:07 AM

Jul 27 2022

blanchette committed rAFP3488d4772567: added lemma about lazy list chains.
added lemma about lazy list chains
Jul 27 2022, 5:25 PM

Jul 26 2022

blanchette committed rAFP0ab6087cd196: typo.
typo
Jul 26 2022, 3:08 PM

Jul 11 2022

blanchette committed rISABELLE707748d3d186: prefer non-JNI SAT solvers by default in Nitpick.
prefer non-JNI SAT solvers by default in Nitpick
Jul 11 2022, 3:04 PM
blanchette committed rISABELLEa65c4539dedb: milder Sledgehammer messages.
milder Sledgehammer messages
Jul 11 2022, 3:04 PM

Apr 13 2022

blanchette committed rISABELLEa36a1cc0144c: pass new option only to new version of E.
pass new option only to new version of E
Apr 13 2022, 4:58 PM

Apr 8 2022

blanchette committed rISABELLE9c0300345e17: enable an E option suggested by Petar Vukmirovic.
enable an E option suggested by Petar Vukmirovic
Apr 8 2022, 5:19 PM

Apr 1 2022

blanchette committed rISABELLE38663b1de300: merge.
merge
Apr 1 2022, 12:28 PM
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
Apr 1 2022, 12:28 PM

Mar 31 2022

blanchette committed rISABELLEbdab2daa2779: further tweaked E's setup.
further tweaked E's setup
Mar 31 2022, 6:20 PM
blanchette committed rISABELLE307a0ae5f978: tweaked E setup.
tweaked E setup
Mar 31 2022, 3:35 PM

Mar 29 2022

blanchette committed rISABELLEcf09060add1c: nicer TPTP output.
nicer TPTP output
Mar 29 2022, 1:59 PM

Mar 25 2022

blanchette committed rISABELLE647611e6da76: compile TPTP module.
compile TPTP module
Mar 25 2022, 1:55 PM
blanchette committed rISABELLE62f0fda48a39: compile mirabelle.
compile mirabelle
Mar 25 2022, 1:55 PM
blanchette committed rISABELLE959a74c665d2: further modernized E setup.
further modernized E setup
Mar 25 2022, 1:55 PM
blanchette committed rISABELLE72cbbb4d98f3: cleaned up obsolete E setup and a bit of SPASS.
cleaned up obsolete E setup and a bit of SPASS
Mar 25 2022, 1:55 PM
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…
Mar 25 2022, 1:55 PM
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…
Mar 25 2022, 1:55 PM
blanchette committed rISABELLE28d2cb99b37f: added parentheses in TPTP output -- seem necessary for some provers.
added parentheses in TPTP output -- seem necessary for some provers
Mar 25 2022, 11:05 AM

Feb 22 2022

blanchette committed rISABELLE18cd39e55eca: have Sledgehammer honor 'smt_nat_as_int' option.
have Sledgehammer honor 'smt_nat_as_int' option
Feb 22 2022, 3:41 PM
blanchette committed rISABELLE66eb6fdfc244: handle Zipperposition definitions in Isar proof construction.
handle Zipperposition definitions in Isar proof construction
Feb 22 2022, 1:01 PM
blanchette committed rISABELLEf12539c8de0c: more handling of Zipperposition definitions in Isar proof construction.
more handling of Zipperposition definitions in Isar proof construction
Feb 22 2022, 1:01 PM
blanchette committed rISABELLE00eeac3fd246: parse Zipperposition definitions.
parse Zipperposition definitions
Feb 22 2022, 10:12 AM

Feb 14 2022

blanchette committed rISABELLE3bcbc4d12916: print outcome of Sledgehammer search in panel.
print outcome of Sledgehammer search in panel
Feb 14 2022, 4:54 PM
blanchette committed rISABELLE27c93bfb0016: print Sledgehammer error message.
print Sledgehammer error message
Feb 14 2022, 4:54 PM

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 9 2022, 11:02 AM

Feb 8 2022

blanchette committed rISABELLE41fd2e8f6b16: more robust TSTP proof parsing.
more robust TSTP proof parsing
Feb 8 2022, 11:41 AM
blanchette committed rISABELLE7ff39293e265: added possibility of extra options to SMT slices.
added possibility of extra options to SMT slices
Feb 8 2022, 11:41 AM

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…
Feb 2 2022, 2:06 PM
blanchette committed rISABELLE5f29ddeb0386: enable induction in one of Zipperposition's slices.
enable induction in one of Zipperposition's slices
Feb 2 2022, 2:06 PM
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…
Feb 2 2022, 10:50 AM
blanchette committed rISABELLE79b4e711d6a2: robustly handle empty proof blocks in Isar proof output.
robustly handle empty proof blocks in Isar proof output
Feb 2 2022, 10:50 AM
blanchette committed rISABELLE04a4881ff0fd: propagate right result when enough proofs have been found.
propagate right result when enough proofs have been found
Feb 2 2022, 10:50 AM
blanchette committed rISABELLEec18dcd6e85f: don't lose error messages.
don't lose error messages
Feb 2 2022, 10:50 AM
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…
Feb 2 2022, 10:50 AM
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…
Feb 2 2022, 10:50 AM