# User Details

User Details

- User Since
- Nov 21 2019, 6:25 PM (67 w, 3 d)

# Nov 30 2020

Nov 30 2020

renamed confusingly named predicate

# Nov 6 2020

Nov 6 2020

renamed t_ functions to T_ (im Auftrag von T. Nipkow)

undid renaming accident

renamed t_ functions to T_ (im Auftrag von T. Nipkow)

# Oct 8 2020

Oct 8 2020

tuned mirabelle documentation

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

removed spurious documentation item

blanchette committed rISABELLE2783779b7dd3: removed obsolete unmaintained experimental prover Pirate.

removed obsolete unmaintained experimental prover Pirate

# Sep 24 2020

Sep 24 2020

simplified proof using Uwe Waldmann's idea + tuning

# Sep 3 2020

Sep 3 2020

# Sep 2 2020

Sep 2 2020

# Sep 1 2020

Sep 1 2020

# Aug 31 2020

Aug 31 2020

tuned arrows, and proofs

# Aug 28 2020

Aug 28 2020

mild renamings in saturation framework

simplified 'length = 0'

# Aug 26 2020

Aug 26 2020

merged two theory files and cleaned up some locales

# Aug 20 2020

Aug 20 2020

removed double underscores + tuned comments

basic integration of Zipperposition 2.0

tuned Mirabelle comments

bring title of document in sync with title of entry

# Jul 6 2020

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…

# Jun 16 2020

Jun 16 2020

eliminated needless locale

more renamings in Saturation Framework

renamed locales as discussed with Sophie Tourret

added file that was part of previous renaming/refactoring

blanchette committed rAFP2f6ec228e270: renamed file in Saturation_Framework following discussion with Sophie Tourret.

renamed file in Saturation_Framework following discussion with Sophie Tourret

# Jun 10 2020

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…

# May 25 2020

May 25 2020

more systematic self-citations

# May 19 2020

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

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

more work on liminf llist library

# May 18 2020

May 18 2020

enriched theorem proving library

# May 15 2020

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…

added lemma about limits

blanchette committed rAFP6c077dc51be0: various extensions and simplifications to the theorem proving libraries.

various extensions and simplifications to the theorem proving libraries

# May 14 2020

May 14 2020

# May 13 2020

May 13 2020

uniformize capitalization

# May 12 2020

May 12 2020

moved lemmas around, tuning

# May 11 2020

May 11 2020

moving lemmas where they belong

generalized completeness theorems + refactored a little

blanchette committed rAFP982c9eb51fe6: rationalized locales.

rationalized locales

blanchette committed rAFPff58aa530358: rationalized locales.

rationalized locales

removed abbreviation that only lengthened formalization

blanchette committed rAFPf67a3c3fcc17: rationalized locales.

rationalized locales

blanchette committed rAFPbb1e74987268: rationalized locales.

rationalized locales

blanchette committed rAFP5058f17437d6: rationalized locales.

rationalized locales

# May 10 2020

May 10 2020

blanchette committed rAFPc9078e5ff173: simplified locale setup + replaced some definitions by abbreviations.

simplified locale setup + replaced some definitions by abbreviations

# May 9 2020

May 9 2020

blanchette committed rAFPfd511536d43d: rationalized locales.

rationalized locales

rationalized locales, reducing aliasing

# May 8 2020

May 8 2020

removed prefixes on key sublocales

blanchette committed rAFPa9a2c8a4527f: added a few theorems about supremum in Ordered_Resolution_Prover.

added a few theorems about supremum in Ordered_Resolution_Prover

added 'sublocale', simplified rest of formalization

# May 6 2020

May 6 2020

added lemma to Ordered_Resolution_Prover

avoid mixture of definitionally equal constants

# May 5 2020

May 5 2020

added lemma to Ordered_Resolution_Prover

removed redundant assumptions

added lemmas about clausal logic

# May 4 2020

May 4 2020

tuning, including a suggestion by Tobias N.

modernized notations in saturation framework

simplify big unions in Saturation_Framework

added a lemma about grounding in ordered resolution prover

generalized framework a little

further generalized framework

avoid spurious dependency

# May 1 2020

May 1 2020

simplified definition

# Apr 30 2020

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

moved lemmas out of scope of needless assumption

blanchette committed rAFP300d01f54b0e: renamed 'generalizes_cls' operation and proved more lemmas about it.

renamed 'generalizes_cls' operation and proved more lemmas about it

# Apr 29 2020

Apr 29 2020

tuning Saturation_Framework

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)

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…

make equivalence a predicate in Saturation_Framework

removed spurious assumption

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 28 2020

Apr 28 2020

removed spurious locale argument

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…

enriched abstract substitution library slightly

blanchette committed rAFPa9b675f61a06: refactoring to make parts of proof reusable to ongoing formalization.

refactoring to make parts of proof reusable to ongoing formalization

# Apr 23 2020

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.

blanchette committed rISABELLEac28714b7478: avoid passing chained facts twice to preplay in Sledgehammer.

avoid passing chained facts twice to preplay in Sledgehammer

tweaked Vampire's options + tuning