Page MenuHomeIsabelle/Phabricator

blanchette (Jasmin Blanchette)
User

Projects

User Details

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

Recent Activity

Wed, Mar 15

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

Fri, Mar 10

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

Wed, Mar 8

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

Fri, Mar 3

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

Wed, Mar 1

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

Mon, Feb 20

blanchette committed rAFP7ff72891adea: tuned metis call to avoid obscure feature.
tuned metis call to avoid obscure feature
Mon, Feb 20, 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
blanchette committed rISABELLE1a8f6cb5efd6: don't perform preplaying steps if preplaying is disabled.
don't perform preplaying steps if preplaying is disabled
Feb 2 2022, 10:50 AM
blanchette committed rISABELLE9e1d486e2d9f: careful with partial applications.
careful with partial applications
Feb 2 2022, 10:50 AM
blanchette committed rISABELLE8ce2469920bf: tuned punctuation.
tuned punctuation
Feb 2 2022, 10:50 AM
blanchette committed rISABELLE632c9ae415fa: adjust TPTP THF parser to give priority to @ over other operators, to parse….
adjust TPTP THF parser to give priority to @ over other operators, to parse…
Feb 2 2022, 10:50 AM
blanchette committed rISABELLEe926618f9474: handle TPTP '!=' more gracefully in Isar proof reconstruction.
handle TPTP '!=' more gracefully in Isar proof reconstruction
Feb 2 2022, 10:50 AM
blanchette committed rISABELLE7d2a5d1f09af: guard against duplicate lines in Zipperposition proofs.
guard against duplicate lines in Zipperposition proofs
Feb 2 2022, 10:50 AM

Feb 1 2022

blanchette committed rISABELLE38e24aeeedb8: compile HOL-TPTP.
compile HOL-TPTP
Feb 1 2022, 9:23 AM
blanchette committed rISABELLE52b37e8a617b: tuning.
tuning
Feb 1 2022, 9:23 AM
blanchette committed rISABELLEf47410c603c6: tuned NEWS.
tuned NEWS
Feb 1 2022, 9:23 AM
blanchette committed rISABELLE46a94aa3ec8e: compile Metis_Examples.
compile Metis_Examples
Feb 1 2022, 9:23 AM
blanchette committed rISABELLE787b69fffaae: more NEWS.
more NEWS
Feb 1 2022, 9:23 AM
blanchette committed rISABELLE094ba0948403: updated NEWS.
updated NEWS
Feb 1 2022, 9:23 AM
blanchette committed rISABELLEa695b78213e5: compile mirabelle.
compile mirabelle
Feb 1 2022, 9:23 AM
blanchette committed rISABELLEfada390d49dd: tweaked Auto Sledgehammer's behavior and output.
tweaked Auto Sledgehammer's behavior and output
Feb 1 2022, 9:23 AM
blanchette committed rISABELLEe5750bcb8c41: removed experimental prover z3_tptp.
removed experimental prover z3_tptp
Feb 1 2022, 9:23 AM