[seqfan] Re: talk announcement: Proving properties of OEIS sequences with Walnut

[hv at crypt.org]

I can imagine such output being of value - as an option of course,
not by default.

The opportunity to check a proof seems critical to me. The easier
it is to check, the greater the confidence we can have in the proof.

Hugo

Jeffrey Shallit <shallit at uwaterloo.ca> wrote:
:Just as a follow-up:Â  a typical Walnut query consists of a parsable 
:logical formula, for example
:something like
:
:For all x there exists y such that f(x,y) holds.
:
:But in Walnut it is easy to assert
:
:1.  f(x,y) holds
:2.  there exists y such that f(x,y) holds
:3.  For all x there exists y such that f(x,y) holds.
:
:And get automata corresponding to each of these.   So Walnut already has 
:the capability to produce the
:automata for individual parts of any expression and these could be 
:considered a certificate
:and each part could then easily be individually checked by another 
:program, if one wanted.
:(But the other program would essentially just be reproducing the 
:calculations of Walnut!)
:
:
:On 2022-10-24 8:19 AM, Jeffrey Shallit wrote:
:>
:>
:> On 2022-10-21 11:21 AM, hv at crypt.org wrote:
:>>
:>> While I know a little about DFAs from my programming work (including
:>> a lot of work on the regexp engine in Perl), I know little about them
:>> mathematically. Is it plausible that Walnut could generate a kind of
:>> certificate by outputting one or more DFAs along with some
:>> canonicalized description of the transformations it is performing
:>> on them?
:>>
:>>
:> Unfortunately that would be (for all practical purposes) just redoing 
:> exactly the same
:> calculation that Walnut is already doing.   And for some of them the 
:> "certificate" would be really huge.
:>
:> So I don't see any point in doing that.
:>
:> -- 
:> Seqfan Mailing list - http://list.seqfan.eu/
:
:
:--
:Seqfan Mailing list - http://list.seqfan.eu/