870: Structural Proof Theory/2

[Wolfgang Windsteiger]

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