User Details
User Details
- User Since
- Nov 21 2019, 6:25 PM (173 w, 4 d)
Wed, Mar 15
Wed, Mar 15
removed accidental junk
Fri, Mar 10
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…
don't try to falisfy goals with schematics
Wed, Mar 8
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
Fri, Mar 3
Fri, Mar 3
blanchette committed rISABELLE8a28ab58d155: detect duplicates in Sledgehammer output -- suggested by Larry Paulson.
detect duplicates in Sledgehammer output -- suggested by Larry Paulson
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…
Wed, Mar 1
Wed, Mar 1
tweaked Sledgehammer interaction
there won't be an E version 2.7
adopt terminology suggested by Larry Paulson
reverted 0506c3273814 -- the message is still useful
more robust E proof parsing
tweaked abduction in Sledgehammer
avoid double 'Warning:' in Sledgehammer messages
slightly more documentation
renamed new Sledgehammer option
updated documentation
improve ad hoc abduction in Sledgehammer
implemented ad hoc abduction in Sledgehammer with E
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'
Mon, Feb 20
Mon, Feb 20
tuned metis call to avoid obscure feature
Feb 15 2023
Feb 15 2023
removed rarely used error in Sledgehammer
blanchette committed rISABELLEbc43f86c9598: added refute mode to Sledgehammer to find 'counterexamples'.
added refute mode to Sledgehammer to find 'counterexamples'
Feb 13 2023
Feb 13 2023
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
Dec 20 2022
Dec 20 2022
added lifting_forget as suggested by Peter Lammich
adapted to Isabelle/c48fe2be847f
Nov 23 2022
Nov 23 2022
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 10 2022
Nov 10 2022
use timeout with MiniSat
Oct 17 2022
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…
Sep 5 2022
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 2 2022
Sep 2 2022
replaced slow smt call by blast
Aug 25 2022
Aug 25 2022
Aug 18 2022
Aug 18 2022
reintroduced SPASS to the mix
Aug 17 2022
Aug 17 2022
tweaked generation of Isar proofs
blanchette committed rISABELLE8bfad7bc74cb: tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and….
tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and…
Aug 16 2022
Aug 16 2022
revived 'try0' and 'smart' Isar proofs in Sledgehammer
Aug 12 2022
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 5 2022
Aug 5 2022
Aug 4 2022
Aug 4 2022
more politically correct
Aug 3 2022
Aug 3 2022
added two lemmas to relational chains
Aug 2 2022
Aug 2 2022
blanchette committed rISABELLE3557f826362c: changed the order of Zipperposition slices in Sledgehammer.
changed the order of Zipperposition slices in Sledgehammer
changed confusing assumption name
Jul 29 2022
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…
removed needless assumption
Jul 27 2022
Jul 27 2022
added lemma about lazy list chains
Jul 26 2022
Jul 26 2022
Jul 11 2022
Jul 11 2022
prefer non-JNI SAT solvers by default in Nitpick
milder Sledgehammer messages
Apr 13 2022
Apr 13 2022
pass new option only to new version of E
Apr 8 2022
Apr 8 2022
enable an E option suggested by Petar Vukmirovic
Apr 1 2022
Apr 1 2022
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
Mar 31 2022
Mar 31 2022
further tweaked E's setup
Mar 29 2022
Mar 29 2022
Mar 25 2022
Mar 25 2022
compile TPTP module
further modernized E setup
cleaned up obsolete E setup and a bit of SPASS
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…
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…
blanchette committed rISABELLE28d2cb99b37f: added parentheses in TPTP output -- seem necessary for some provers.
added parentheses in TPTP output -- seem necessary for some provers
Feb 22 2022
Feb 22 2022
have Sledgehammer honor 'smt_nat_as_int' option
blanchette committed rISABELLE66eb6fdfc244: handle Zipperposition definitions in Isar proof construction.
handle Zipperposition definitions in Isar proof construction
blanchette committed rISABELLEf12539c8de0c: more handling of Zipperposition definitions in Isar proof construction.
more handling of Zipperposition definitions in Isar proof construction
parse Zipperposition definitions
Feb 14 2022
Feb 14 2022
print outcome of Sledgehammer search in panel
print Sledgehammer error message
Feb 9 2022
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 8 2022
Feb 8 2022
more robust TSTP proof parsing
added possibility of extra options to SMT slices
Feb 2 2022
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…
enable induction in one of Zipperposition's slices
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…
blanchette committed rISABELLE79b4e711d6a2: robustly handle empty proof blocks in Isar proof output.
robustly handle empty proof blocks in Isar proof output
blanchette committed rISABELLE04a4881ff0fd: propagate right result when enough proofs have been found.
propagate right result when enough proofs have been found
don't lose error messages
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…
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…
blanchette committed rISABELLE1a8f6cb5efd6: don't perform preplaying steps if preplaying is disabled.
don't perform preplaying steps if preplaying is disabled
careful with partial applications
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…
blanchette committed rISABELLEe926618f9474: handle TPTP '!=' more gracefully in Isar proof reconstruction.
handle TPTP '!=' more gracefully in Isar proof reconstruction
guard against duplicate lines in Zipperposition proofs
Feb 1 2022
Feb 1 2022
compile Metis_Examples
tweaked Auto Sledgehammer's behavior and output
removed experimental prover z3_tptp