870: Structural Proof Theory/2
Wolfgang Windsteiger
Wolfgang.Windsteiger at risc.jku.at
Tue Mar 23 05:43:42 EDT 2021
On 22.03.21 12:09, Mario Carneiro wrote:
> On Sun, Mar 21, 2021 at 9:56 PM Buzzard, Kevin M <k.buzzard at imperial.ac.uk>
> wrote:
>
>> KB: Commutativity is harder because it involves
>> discovering an idea which you don't mention: Sa + b = S(a+b).
>>
>
>> KB: I would say that commutativity of addition requires an idea.
>>
> Try proving it by induction yourself -- you run into an issue.
>> The art is to build up the right theorems in the right order.
>>
>
> I would say that commutativity can also be done by "following your nose",
> but it requires some higher order thinking. Specifically, you can do the
> straightforward proof by induction, and you will get stuck, and you can
> isolate the issue to exactly the statement Sa + b = S(a+b). So you
> conjecture it, see that it's true for small numbers, and then try to prove
> it by induction, which succeeds. (I believe you have to do this in the base
> case as well, where 0 + n = n shows up.) I'm not sure what the state of the
> art is regarding deriving new conjectures from proof failures (which can be
> tough because there are lots of reasons a proof can fail and most of them
> are not interesting from a conjecture making POV).
We did this thing in an automated way in the Theorema system many years
ago, it was called the "Cascade" and the "Lazy Thinking Paradigm": In a
nutshell, repeat the following steps:
1) Do an automated proof
2a) if it succeeds, add the statement to the knowledge base
2b) if it fails, analyze the failure (also for failing proofs, we have a
proof object, that contains the proof situation, where the prover could
not continue)
3) Generate a conjecture by generalizing the failing proof situation
4) Proof the conjecture by recursive application of the same strategy.
Commutativity of + in the natural numbers was one of the easy ones. But
Lazy Thinking has been driven as far as to completely "re-invent" the
algorithm for computing Groebner bases in a fully automated way. One of
the relevant papers is
B. Buchberger Towards the Automated Synthesis of a Groebner Bases
Algorithm. RACSAM - Revista de la Real Academia de Ciencias (Review of
the Spanish Royal Academy of Science), Serie A: Mathematicas 98(1), pp.
65-75. 2004. ISSN 1578 7303.
but if you google "Buchberger Lazy Thinking" you find lots of talks
where this principle is explained in more details.
WW.
--
Assoc.Univ.-Prof. DI Dr. Wolfgang Windsteiger
RISC Institute / JKU Linz
Castle Hagenberg, 4232 Hagenberg i.M., Austria
Phone: +43 732 2468-9960
http://www.risc.jku.at/home/wwindste/
PGP: find the public key on my homepage
More information about the FOM
mailing list