Todd Wilson
Todd Wilson
Can the tutorial be amended to include an example of how to do pre-computation before gathering benchmark data? For example, suppose my benchmark is mapping a function across several lists...
Given that one of the possible witnesses is `unfold(id,n,witness1,...,witnessn)` (where the second `n` should really be `k`), wouldn't it make sense to have a tactic `unfold id n`, so that...
In an earlier version of Abella, the searches in this (small) theorem completed almost instantly with the witnesses indicated in the comments. Now they hang, or at least take more...
Sorry for dropping into the middle of a proof, but a single proof state should be enough to illustrate my problem (in Abella 2.0.5): ``` Variables: G R G' T...
A student wrote a simple recursive addition predicate and used `Query` to verify 1 + 2 = 3, but failed to find any solution to 1 + 3 = ?....
When I requested, in version 1.3, that Andrew introduce an option to print search witnesses, he did a wonderful job that exceeded my expectations. Since then, it has been a...
It would be nice if Abella allowed as aliases for `Theorem` the commands `Lemma`, `Proposition`, `Corollary`, `Example`, `Conjecture` (and others I might be overlooking). Also, Abella used to have a...
I find the new `instantiations` flag useful to help figure out what case I'm in during a proof. However, this would be even more useful if, in addition to the...
Using 2.0.3, I notice that a couple of error messages do not provide information on either the offending source file or line and character numbers: - Error: Failure("Unknown constant: ??")...
The Eight Queens program included in Examples (citation: O'Keefe, The Craft of Prolog) is unnecessarily complicated and wasteful in its data structure. Here is a much simpler program that uses...