--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
...
I've also thought about attacking the problem of learning set.mm Propositional Logic from QED or The Incredible Proof machine the other way around. I could take the set.mm proof of, say, Peirce's Law and break it into smaller pieces until it starts to resemble my QED proof of Peirce's Law or my Incredible Proof Machine proof of Peirce's Law.
'peirce' uses 'simplim', 'id', and 'ja'
'simplim' uses 'pm2.21', and 'con1i'
So the first step would be to splice 'peirce' and 'simplim' together in order to express 'perice' in terms of 'pm2.21', 'con1i', 'id', and 'ja'. I can just about manage to do that sort of thing manually, but is there code that automates this operation, please?
peirce.splice1 $p |- ( ( ( ph -> ps ) -> ph ) -> ph ) $=
wph wps wi wph wph wph wph wps wi wph wps pm2.21 con1i wph id ja $.
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
Dear Norm,That's wonderful, thank you!I've tried that on contrapositioncon3 $p |- ( ( ph -> ps ) -> ( -. ps -> -. ph ) ) $=
( wi id con3d ) ABCZABFDE $.and I get 213 steps from the axioms.
So it might interest you that someone's managed it in 72 steps!
DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D1DD2D1311 – 43 steps
DD2D1DD2D1DD2DD2D13D2DD2D1311DD22D1DD2D1311 – also 43 steps
Separately, I tried to find a short proof by hand. and found yet another 43-step proof:
DD2D1DD2DD2D13D2DD2D1311DD2DD2D121D1DD2D131
Norm
Here's an experiment to take expansion to the extreme and obtain a proof directly from axioms.
MM> prove peirce
(As indicated in my previous post, here is George's description of his "genetic algorithm", copied from his email to me of 5/21/18. -Norm)
Below, I give a short summary and explanation of the algorithm.
population = CreatePrototypes()
population = InsertRussellWhitehead(population)
for generation in range(0,NrOfGenerations):
population = Ranking(population)
population = RemoveTwins(population)
population = Mutations(population)
population = FormCouples(population)
population = Renewal(population)
population = NextGen(population)
CreatePrototypes: 199 prototypes strings of the ‘symmetric tree’ form are created to form the population:
DDDDjkDjkDDjkDjkDDDjkDjkDDjkDjk.
j and k stand for axioms 1, 2 and 3. Each time a protoype is created, it is tested with drule to see whether it is a ‘legitimate’ string.
(It takes approximately 40,000 prototypes to obtain 200 legitimate prototypes of the above form; i..e, about 0.5 percent of the attempts are legitimate.)
InsertRussellWhitehead: the string from pmproofs that is thought to be the shortest, is entered into the population. E.g. Theorem 1:4: DD2D13D2D1D3DD2DD2D13DD2D1311
The theorem (i.e. the output of drule when it is run with RussellWhitehead as an input) is entered in reverse Polish notation as the ‘target’.
E.g.: Theorem 1.4: >>~PQ>~QP
Ranking: drule is run with all strings. (I use the word ‘string’ now. ‘Prototype’ is when a new string is created) The strings are ranked according to how much the results (the outputs of drule) overlap with the target. That is the ‘fitness’. (More on fitness below).
Of course, RussellWhitehead is ranked first because 100% of its output overlaps with the target.
RemoveTwins: after a few generations, it often happens that a large part of the population is identical to RussellWhitehead or to some other highly-ranked string. To prevent that the entire population becomes largely homogenous, only one copy of such strings are kept. The other copies are deleted and replaced with new prototypes. (Each new prototype ios tested, as usual, with drule to check that it is legitimate.) Thus, diversity of the population is guaranteed.
Mutations: a certain percentage of the j’s and k’s are randomly mutated into any other axiom. Again, all such mutated strings are tested with drule and if the string is ‘illegitimate’ another mutation is attempted. The three top-ranked strings are exempt from mutation, so they do not get lost inadvertently.
FormCouples:
The top-ranked quarter of the strings are the ‘dads’. Each dad randomly choses a ‘mom’ from the lower-ranked strings, with more weight being given to higher ranked moms.
Renewal: the strings ranked in the bottom quarter are discarded and replaced by new prototypes. (Tested with drule) This increases the population’s diversity.
NexGen: THIS IS THE CRUX OF THE ALGORITHM
Our population consists of 200 strings of the forms:
aaaaaaaaaaaaaaaaaaaaaaaa
BBBBBBBBBBBBBBB
…
Then, each pair of parents create two offspring through ‘crossover’. I.e., chunks are randomly chosen and exchanged:
aaaaBBBBaaaaaaaaa
BBBBBBBaaaaaaaaBBBB….
The chunks that are exchanged must have an equal number of D’s and axioms 1,2,3. The resulting offspring are tested with drule. If they are illegitimate, the crossover is run again, until the offspring are legitimate.
Then we go on to the next generation. I usually run between 500 and 200 generations. (about 30 seconds per generation).
A remark on fitness: the algorithm aims for two things: the overlap should eventually become 100% and the string should be as short as possible. I have tried various forms of fitness functions and what seems to work well is:
(Percentage of overlap) * (Length of overlap)^2
(length of the drule-result)^0.33
Results:
So far, I only found two strings that are shorter than the ones listed on pmproofs (Meredith and 3.37). This may mean that the algorithm is not very effective in finding shorter strings or, what I suspect, the strings listed on pmproofs are, indeed the shortest ones.
What gives me confidence in the algorithm is that it found several strings that were as long as – but different from – the shortest string listed. For example, for theorem 4.73 it found three additional strings of length 113 which result in >P~>>Q~>Q~P~>~>RSR:
DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D13DD2D1D2DD2DD2D1DD2D1331111D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131
DD2DD2D13DD2D1DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D13DD2D1D2DD2DD2D1DD2D1331111D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131
DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111D1D3DD2D1D3DD2DD2D1DD2D13311DD2D131