All of the lemmas involved are either arihmetic or logical inference
rules and make sense. Presburger is a generic and complex decision
procedure. I am not surprised and would not want to optimize presburger
to use fewer lemmas.
Tobias
Am 28/06/2011 00:08, schrieb Jasmin Blanchette:
Hi all,
Hi all,
Quick question: Josef Urban noticed that the proof terms for some lemmas proved
directly by "presburger" can refer to lots of other lemmas; for example, the
proof of "Parity.even_mult_two_ex" directly refers to 206 lemmas.
ML {* Thm.proof_body_of @{thm Parity.even_mult_two_ex} *}
(I've
Jasmin Blanchette wrote:
This motivates me to attack the "linarith" problem. If nobody
objects, I'll call the property "linarith_verbose" and have it on by
default (for compatibility) but off in "try_methods" and "try". I've
also taken the liberty to reword the "counterexample trace" message
>> you get the warning
>>
>> ### Metis: Unused theorems: "List.map.simps_2"
>>
>> which is strange because in Metis's code that warning is only printed if
>> "verbose" is true. Is "Proof.map_context" not the thing I should be using?
>
> Proof.map_context is right, also the use of the context
Hi all,
E 1.3 was secretly released on Sunday, and with it an extremely cool feature:
"Weight functions that allow the user to focus the search on certain function
symbols" [1]. This feature was motivated by Sledgehammer and is used for all
its worth so that those lemmas that seem more relevant
On Sun, 26 Jun 2011, Jasmin Christian Blanchette wrote:
Now, this all sounds well and good, but there is a little glitch. In
"try_methods.ML" the line
val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose
false)
is meant to tell Metis to be quiet, but somehow it is ignored.
Am 24.06.2011 um 11:32 schrieb Lukas Bulwahn:
> I only noticed that using "try" you often get a misleading response from
> linarith that "linarith found a counterexample" which beginners might stumble
> on.
> It might be better to switch off this warning by default (and offer a
> configuration
On Sun, 26 Jun 2011, Alexander Krauss wrote:
Given to bindings (i.e., instances of Binding.binding), how are they
supposed to be compared?
Here is a more concrete example. Assume there is a declaration such
as:
declare_foo name = ...
which declares "name" as some new foo-entity. For late
