Page MenuHomeIsabelle/Phabricator

blanchette (Jasmin Blanchette)
User

Projects

User Details

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

Recent Activity

Fri, Aug 27

blanchette committed rISABELLE1a8d8dd77513: made sure lambda-lifting works well with native let binders in Sledgehammer.
made sure lambda-lifting works well with native let binders in Sledgehammer
Fri, Aug 27, 8:57 PM
blanchette committed rISABELLEadf767b94f77: handle Zipperposition's ResourceOut gracefully.
handle Zipperposition's ResourceOut gracefully
Fri, Aug 27, 2:50 PM
blanchette committed rISABELLE9c6159cbf9ee: disabled 'ite' in Zipperposition until we upgrade to a version of Zip that….
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that…
Fri, Aug 27, 2:50 PM

Jul 19 2021

blanchette committed rISABELLEd0b190b4f15d: parse TPTP operator @ also when not parenthesized.
parse TPTP operator @ also when not parenthesized
Jul 19 2021, 7:00 PM
blanchette committed rISABELLEbed899f14df7: tuning.
tuning
Jul 19 2021, 7:00 PM
blanchette committed rISABELLEa2b470e315ee: tuned E's lambda encoding.
tuned E's lambda encoding
Jul 19 2021, 7:00 PM
blanchette committed rISABELLEa0c9fc9c7dbe: removed setup for outdated CVC3 from Isabelle.
removed setup for outdated CVC3 from Isabelle
Jul 19 2021, 7:00 PM
blanchette committed rISABELLE462d652ad910: use Vampire's clausifier with iProver, now that E's is no longer supported.
use Vampire's clausifier with iProver, now that E's is no longer supported
Jul 19 2021, 10:46 AM
blanchette committed rISABELLE302994f5a3c2: updated Sledgehammer docs -- removed most version numbers since these are….
updated Sledgehammer docs -- removed most version numbers since these are…
Jul 19 2021, 10:46 AM
blanchette committed rISABELLE943757b788f9: compile.
compile
Jul 19 2021, 10:03 AM

Jul 16 2021

blanchette committed rISABELLE1a0a536b8aaf: removed support for experimental Pirate prover.
removed support for experimental Pirate prover
Jul 16 2021, 4:25 PM
blanchette committed rISABELLE14de47e29fe4: get rid of remote_vampire since it's hard, if possible at all, to follow….
get rid of remote_vampire since it's hard, if possible at all, to follow…
Jul 16 2021, 3:41 PM
blanchette committed rAFP11e377bef9e9: compile.
compile
Jul 16 2021, 9:35 AM

Jul 15 2021

blanchette committed rISABELLE84528a343f5f: extended the 'corec' format slightly.
extended the 'corec' format slightly
Jul 15 2021, 4:21 PM

Jul 14 2021

blanchette committed rISABELLE291f7b5fc7c9: prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent.
prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent
Jul 14 2021, 4:24 PM
blanchette committed rISABELLEe5322146e7e8: tuning.
tuning
Jul 14 2021, 4:24 PM
blanchette committed rISABELLE906ecb049141: rephrase Nitpick constraint in more first-order format that's also more….
rephrase Nitpick constraint in more first-order format that's also more…
Jul 14 2021, 2:32 PM
blanchette committed rISABELLE2d8a0f8e30ec: correctly translate constructor argument in 'primrec'.
correctly translate constructor argument in 'primrec'
Jul 14 2021, 10:04 AM

Jul 13 2021

blanchette committed rISABELLE8d93f9ca6518: revisited ac28714b7478: more faithful preplaying with chained facts.
revisited ac28714b7478: more faithful preplaying with chained facts
Jul 13 2021, 10:59 AM
blanchette committed rISABELLEf0d231ead660: added alternative E binary name.
added alternative E binary name
Jul 13 2021, 10:59 AM
blanchette committed rISABELLE6a0e1c14a8c2: wait for E 2.7 before using 'ite' in HO mode.
wait for E 2.7 before using 'ite' in HO mode
Jul 13 2021, 10:59 AM

Jul 12 2021

blanchette committed rISABELLEb304285fd800: parse logical operators in the right order w.r.t. backtracking.
parse logical operators in the right order w.r.t. backtracking
Jul 12 2021, 4:32 PM
blanchette committed rISABELLE34c8cf767fa3: adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing).
adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing)
Jul 12 2021, 4:32 PM
blanchette committed rISABELLE96a05b8462f9: improved warning.
improved warning
Jul 12 2021, 4:32 PM

Nov 30 2020

blanchette committed rAFP391fd487234d: renamed confusingly named predicate.
renamed confusingly named predicate
Nov 30 2020, 8:08 PM

Nov 6 2020

blanchette committed rAFPdf1eba12de1c: renamed t_ functions to T_ (im Auftrag von T. Nipkow).
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
Nov 6 2020, 1:04 PM
blanchette committed rISABELLE729d45c7ff33: undid renaming accident.
undid renaming accident
Nov 6 2020, 1:00 PM
blanchette committed rISABELLE1d0ae7e578a0: renamed t_ functions to T_ (im Auftrag von T. Nipkow).
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
Nov 6 2020, 1:00 PM

Oct 8 2020

blanchette committed rISABELLE31ddd23965e6: tuned mirabelle documentation.
tuned mirabelle documentation
Oct 8 2020, 6:35 PM
blanchette committed rISABELLE4a3169d8885c: removed support for obsolete prover SNARK and underperforming prover E-Par.
removed support for obsolete prover SNARK and underperforming prover E-Par
Oct 8 2020, 6:35 PM
blanchette committed rISABELLE148e8332a8b1: removed spurious documentation item.
removed spurious documentation item
Oct 8 2020, 6:35 PM
blanchette committed rISABELLE2783779b7dd3: removed obsolete unmaintained experimental prover Pirate.
removed obsolete unmaintained experimental prover Pirate
Oct 8 2020, 6:35 PM

Sep 24 2020

blanchette committed rAFP3f6499d19e84: simplified proof using Uwe Waldmann's idea + tuning.
simplified proof using Uwe Waldmann's idea + tuning
Sep 24 2020, 2:39 PM

Sep 3 2020

blanchette committed rAFP0a2b5e06621c: renamings.
renamings
Sep 3 2020, 4:31 PM

Sep 2 2020

blanchette committed rAFP075c0450120d: tuned notation.
tuned notation
Sep 2 2020, 4:43 PM

Sep 1 2020

blanchette committed rAFPa22073e6cb92: tuning.
tuning
Sep 1 2020, 11:00 AM

Aug 31 2020

blanchette committed rAFPf22a73cc49a1: tuned arrows, and proofs.
tuned arrows, and proofs
Aug 31 2020, 11:30 AM

Aug 28 2020

blanchette committed rAFPbfee570e953e: mild renamings in saturation framework.
mild renamings in saturation framework
Aug 28 2020, 4:13 PM
blanchette committed rAFP9f61d06c57fc: simplified 'length = 0'.
simplified 'length = 0'
Aug 28 2020, 9:07 AM

Aug 26 2020

blanchette committed rAFPc1979202233d: tuned document.
tuned document
Aug 26 2020, 5:28 PM
blanchette committed rAFPe4e449d5b763: merged two theory files and cleaned up some locales.
merged two theory files and cleaned up some locales
Aug 26 2020, 5:26 PM

Aug 20 2020

blanchette committed rAFP7d42634829a4: removed double underscores + tuned comments.
removed double underscores + tuned comments
Aug 20 2020, 2:28 PM
blanchette committed rISABELLE585b877df698: basic integration of Zipperposition 2.0.
basic integration of Zipperposition 2.0
Aug 20 2020, 12:07 PM
blanchette committed rISABELLE618a0ab13868: tuned Mirabelle comments.
tuned Mirabelle comments
Aug 20 2020, 12:06 PM
blanchette committed rAFP52090471320f: bring title of document in sync with title of entry.
bring title of document in sync with title of entry
Aug 20 2020, 11:48 AM

Jul 6 2020

blanchette committed rISABELLE3e08311ada8e: removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible….
removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible…
Jul 6 2020, 4:53 PM

Jun 16 2020

blanchette committed rAFP06ca7a66d8ae: eliminated needless locale.
eliminated needless locale
Jun 16 2020, 2:55 PM
blanchette committed rAFP14cbc379a00b: more renamings in Saturation Framework.
more renamings in Saturation Framework
Jun 16 2020, 2:41 PM
blanchette committed rAFPe2b1021fb667: renamed locales as discussed with Sophie Tourret.
renamed locales as discussed with Sophie Tourret
Jun 16 2020, 2:20 PM
blanchette committed rAFPc2f07427be69: added file that was part of previous renaming/refactoring.
added file that was part of previous renaming/refactoring
Jun 16 2020, 2:20 PM
blanchette committed rAFP2f6ec228e270: renamed file in Saturation_Framework following discussion with Sophie Tourret.
renamed file in Saturation_Framework following discussion with Sophie Tourret
Jun 16 2020, 2:04 PM

Jun 10 2020

blanchette committed rISABELLE0c8a9c028304: simplified 'smt_proofs' option to be a binary option (instead of ternary), now….
simplified 'smt_proofs' option to be a binary option (instead of ternary), now…
Jun 10 2020, 3:58 PM

May 25 2020

blanchette committed rAFP5a77ba9e257f: more systematic self-citations.
more systematic self-citations
May 25 2020, 9:43 AM

May 19 2020

blanchette committed rAFPc6352b79465d: use lhd and lnull rather than lnth 0 and llength = 0 in IsaFoL.
use lhd and lnull rather than lnth 0 and llength = 0 in IsaFoL
May 19 2020, 5:30 PM
blanchette committed rAFP12e81252fc8d: merged two files that used to be split for technical/political reasons.
merged two files that used to be split for technical/political reasons
May 19 2020, 9:41 AM
blanchette committed rAFP00c6b844e775: more work on liminf llist library.
more work on liminf llist library
May 19 2020, 9:34 AM

May 18 2020

blanchette committed rAFP9df178c7dd08: enriched theorem proving library.
enriched theorem proving library
May 18 2020, 5:07 PM

May 15 2020

blanchette committed rAFPbca5d31690de: moved theory files from IsaFoL repository to AFP now that IsaFoR's KBO is in….
moved theory files from IsaFoL repository to AFP now that IsaFoR's KBO is in…
May 15 2020, 6:39 PM
blanchette committed rAFP2fb9e44335af: merge.
merge
May 15 2020, 1:11 PM
blanchette committed rAFP1e1d92130953: added two lemmas.
added two lemmas
May 15 2020, 1:11 PM
blanchette committed rAFPa3c410f7ad14: merge.
merge
May 15 2020, 10:35 AM
blanchette committed rAFPafa6f540c178: added lemma about limits.
added lemma about limits
May 15 2020, 10:35 AM
blanchette committed rAFP6c077dc51be0: various extensions and simplifications to the theorem proving libraries.
various extensions and simplifications to the theorem proving libraries
May 15 2020, 7:24 AM

May 14 2020

blanchette committed rAFP3483f9d26850: added lemmas.
added lemmas
May 14 2020, 4:32 PM
blanchette committed rAFP68699ec0d47e: tuning.
tuning
May 14 2020, 3:05 PM
blanchette committed rAFPf4451bba95a2: simplified proof.
simplified proof
May 14 2020, 12:03 PM

May 13 2020

blanchette committed rAFPb5739aa85c75: uniformize capitalization.
uniformize capitalization
May 13 2020, 2:57 PM
blanchette committed rAFPf01859e37d6b: added lemmas.
added lemmas
May 13 2020, 11:53 AM

May 12 2020

blanchette committed rAFP55c932d460f7: about to give up.
about to give up
May 12 2020, 6:05 PM
blanchette committed rAFP8274c4ccd8c9: moved lemmas around, tuning.
moved lemmas around, tuning
May 12 2020, 10:48 AM

May 11 2020

blanchette committed rAFP3a7847bc58ce: moving lemmas where they belong.
moving lemmas where they belong
May 11 2020, 10:20 PM
blanchette committed rAFPee34afb2b57c: added lemmas.
added lemmas
May 11 2020, 6:26 PM
blanchette committed rAFP035769df3336: generalized completeness theorems + refactored a little.
generalized completeness theorems + refactored a little
May 11 2020, 5:48 PM
blanchette committed rAFP77ad5390bcd8: added lemmas.
added lemmas
May 11 2020, 5:48 PM
blanchette committed rAFPa7dec07bb044: added two lemmas.
added two lemmas
May 11 2020, 3:11 PM
blanchette committed rAFP2e7ac4fd9a3f: simplified proof.
simplified proof
May 11 2020, 11:32 AM
blanchette committed rAFP982c9eb51fe6: rationalized locales.
rationalized locales
May 11 2020, 11:32 AM
blanchette committed rAFPff58aa530358: rationalized locales.
rationalized locales
May 11 2020, 11:32 AM
blanchette committed rAFP4c337328e727: removed abbreviation that only lengthened formalization.
removed abbreviation that only lengthened formalization
May 11 2020, 11:32 AM
blanchette committed rAFPf67a3c3fcc17: rationalized locales.
rationalized locales
May 11 2020, 11:32 AM
blanchette committed rAFPbb1e74987268: rationalized locales.
rationalized locales
May 11 2020, 11:32 AM
blanchette committed rAFP5058f17437d6: rationalized locales.
rationalized locales
May 11 2020, 7:17 AM

May 10 2020

blanchette committed rAFPc9078e5ff173: simplified locale setup + replaced some definitions by abbreviations.
simplified locale setup + replaced some definitions by abbreviations
May 10 2020, 9:03 PM

May 9 2020

blanchette committed rAFPfd511536d43d: rationalized locales.
rationalized locales
May 9 2020, 10:01 PM
blanchette committed rAFP5ded9bf522f3: rationalized locales, reducing aliasing.
rationalized locales, reducing aliasing
May 9 2020, 10:01 PM

May 8 2020

blanchette committed rAFP08aac5b9f7c0: removed prefixes on key sublocales.
removed prefixes on key sublocales
May 8 2020, 7:51 PM
blanchette committed rAFPa9a2c8a4527f: added a few theorems about supremum in Ordered_Resolution_Prover.
added a few theorems about supremum in Ordered_Resolution_Prover
May 8 2020, 6:14 PM
blanchette committed rAFP9cc7791da210: added 'sublocale', simplified rest of formalization.
added 'sublocale', simplified rest of formalization
May 8 2020, 6:14 PM

May 6 2020

blanchette committed rAFPc50300e44852: added lemma to Ordered_Resolution_Prover.
added lemma to Ordered_Resolution_Prover
May 6 2020, 2:18 PM
blanchette committed rAFPcf6ff7e1b205: avoid mixture of definitionally equal constants.
avoid mixture of definitionally equal constants
May 6 2020, 9:46 AM

May 5 2020

blanchette committed rAFP3f7b5a2543fb: added lemma to Ordered_Resolution_Prover.
added lemma to Ordered_Resolution_Prover
May 5 2020, 5:56 PM
blanchette committed rAFP768f1f3920a4: removed redundant assumptions.
removed redundant assumptions
May 5 2020, 5:33 PM
blanchette committed rAFP4794b1c8b316: getting closer.
getting closer
May 5 2020, 4:15 PM
blanchette committed rAFP8a24d935ee2f: added lemmas about clausal logic.
added lemmas about clausal logic
May 5 2020, 8:29 AM

May 4 2020

blanchette committed rAFP9f7d93d1e881: merge.
merge
May 4 2020, 9:54 PM
blanchette committed rAFPa1646dae4b28: tuning, including a suggestion by Tobias N..
tuning, including a suggestion by Tobias N.
May 4 2020, 9:54 PM
blanchette committed rAFP58e8a311421f: modernized notations in saturation framework.
modernized notations in saturation framework
May 4 2020, 9:01 PM
blanchette committed rAFP4d303d705c38: merge.
merge
May 4 2020, 9:01 PM
blanchette committed rAFP3d6049bb252d: simplify big unions in Saturation_Framework.
simplify big unions in Saturation_Framework
May 4 2020, 9:01 PM
blanchette committed rAFPb60536a943f4: added a lemma about grounding in ordered resolution prover.
added a lemma about grounding in ordered resolution prover
May 4 2020, 9:01 PM