Page MenuHomeIsabelle/Phabricator

blanchette (Jasmin Blanchette)
User

Projects

User Details

User Since
Nov 21 2019, 6:25 PM (37 w, 20 h)

Recent Activity

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
blanchette committed rAFP2f093e52d102: generalized framework a little.
generalized framework a little
May 4 2020, 9:01 PM
blanchette committed rAFP105389413700: further generalized framework.
further generalized framework
May 4 2020, 9:01 PM
blanchette committed rAFP3a4f60720188: shorter name.
shorter name
May 4 2020, 9:01 PM
blanchette committed rAFP7a8a0cafd5dd: avoid spurious dependency.
avoid spurious dependency
May 4 2020, 9:01 PM
blanchette committed rAFP79bdf1d734fc: tuning.
tuning
May 4 2020, 9:01 PM

May 1 2020

blanchette committed rAFP464ed89bce59: simplified definition.
simplified definition
May 1 2020, 7:32 AM

Apr 30 2020

blanchette committed rAFP08eda9f09f3c: introduce more sublocales, since these are useful for users of the framework.
introduce more sublocales, since these are useful for users of the framework
Apr 30 2020, 5:40 PM
blanchette committed rAFPe0809cb242a2: moved lemmas out of scope of needless assumption.
moved lemmas out of scope of needless assumption
Apr 30 2020, 5:06 PM
blanchette committed rAFP300d01f54b0e: renamed 'generalizes_cls' operation and proved more lemmas about it.
renamed 'generalizes_cls' operation and proved more lemmas about it
Apr 30 2020, 12:29 PM

Apr 29 2020

blanchette committed rAFP5e97b5d46902: tuning Saturation_Framework.
tuning Saturation_Framework
Apr 29 2020, 9:49 PM
blanchette committed rAFPc6b2b3c9c949: weakened assumption a tiny bit (syntactically; semantically this is the same).
weakened assumption a tiny bit (syntactically; semantically this is the same)
Apr 29 2020, 6:28 PM
blanchette committed rAFP6b583455e33e: repaired fatal typo in assumption ('equiv_F' vs. 'Equiv_F') and deal with the….
repaired fatal typo in assumption ('equiv_F' vs. 'Equiv_F') and deal with the…
Apr 29 2020, 5:03 PM
blanchette committed rAFP6c23bafd5be8: make equivalence a predicate in Saturation_Framework.
make equivalence a predicate in Saturation_Framework
Apr 29 2020, 2:53 PM
blanchette committed rAFP0019b46607c4: tuning.
tuning
Apr 29 2020, 1:57 PM
blanchette committed rAFPf97be2071061: removed spurious assumption.
removed spurious assumption
Apr 29 2020, 12:40 PM
blanchette committed rAFPc582b55a36c3: tuning.
tuning
Apr 29 2020, 12:28 PM
blanchette committed rAFP68c249f8d1ba: generalized Saturation_Framework a little, to repair a mismatch with the pen….
generalized Saturation_Framework a little, to repair a mismatch with the pen…
Apr 29 2020, 12:13 PM

Apr 28 2020

blanchette committed rAFP8248dddd8b5d: removed spurious locale argument.
removed spurious locale argument
Apr 28 2020, 5:35 PM
blanchette committed rAFP80a3e62140de: generalized saturation framework theory a little, by using spurious 'Q' as a….
generalized saturation framework theory a little, by using spurious 'Q' as a…
Apr 28 2020, 5:21 PM
blanchette committed rAFP6449004f608b: enriched abstract substitution library slightly.
enriched abstract substitution library slightly
Apr 28 2020, 9:17 AM
blanchette committed rAFPa9b675f61a06: refactoring to make parts of proof reusable to ongoing formalization.
refactoring to make parts of proof reusable to ongoing formalization
Apr 28 2020, 8:53 AM

Apr 23 2020

blanchette added a comment to T20: Sledgehammer/z3: "bad SMT term: _".

The heart of the problem is that reconstruction for bit vectors isn't supported (despite the completely wrong and misleading claims made by a certain CPP 2011 papers, due to magical thinking on the part of its authors). We could try to have nicer error messages for that case but it's a bit tricky to do cleanly and without breaking anything. I'll wait to see if it emerges again on the mailing list first.

Apr 23 2020, 5:58 PM
blanchette committed rISABELLEac28714b7478: avoid passing chained facts twice to preplay in Sledgehammer.
avoid passing chained facts twice to preplay in Sledgehammer
Apr 23 2020, 4:52 PM
blanchette committed rISABELLEe771b8157fc7: tweaked Vampire's options + tuning.
tweaked Vampire's options + tuning
Apr 23 2020, 3:46 PM
blanchette committed rAFP8832fd9452c0: clean up TODOs.
clean up TODOs
Apr 23 2020, 2:11 PM
blanchette committed rAFP8fdbf93f3404: cleanup, guided by old FIXMEs.
cleanup, guided by old FIXMEs
Apr 23 2020, 12:38 PM

Apr 22 2020

blanchette committed rAFP34620ae99267: added lemma.
added lemma
Apr 22 2020, 11:35 PM
blanchette committed rAFP8debf0ad489a: tuning.
tuning
Apr 22 2020, 2:36 PM

Apr 21 2020

blanchette committed rAFPf2adcf6df63e: tuning.
tuning
Apr 21 2020, 5:58 PM
blanchette committed rAFP00e9bcef9f32: tuned whitespace.
tuned whitespace
Apr 21 2020, 5:08 PM
blanchette committed rAFP147d3348cd4e: generalized theorem (done by Sophie Tourret) + whitespace tuning.
generalized theorem (done by Sophie Tourret) + whitespace tuning
Apr 21 2020, 5:07 PM
blanchette committed rAFPbc77e51ccd65: tuning + added a lemma proposed by Sophie Tourret.
tuning + added a lemma proposed by Sophie Tourret
Apr 21 2020, 4:57 PM
blanchette committed rAFP2f1b1f57bd12: moved lemma where it belonged.
moved lemma where it belonged
Apr 21 2020, 3:56 PM

Apr 17 2020

blanchette committed rISABELLE3b36fc4916af: removed LaTeX package and hack to avoid ALLCAPS headers.
removed LaTeX package and hack to avoid ALLCAPS headers
Apr 17 2020, 5:32 PM
blanchette committed rISABELLEc7d19729456c: use friendlier package.
use friendlier package
Apr 17 2020, 5:20 PM

Jan 7 2020

blanchette committed rISABELLE475b2260b9c4: removed experimental option to SPASS.
removed experimental option to SPASS
Jan 7 2020, 4:33 PM

Dec 13 2019

blanchette committed rAFPaecde7853101: tuning.
tuning
Dec 13 2019, 11:02 AM