๐ฒ
/
๐๐ยท
I'm generalizing the way I validate proof steps so inference rules match if any formulae with an equivalent (Sapphire specific) normal form would have matched.
๐ณ
/
๐๐ยท
This page is a rough (perhaps embarrassingly so) version of a solution to the first puzzle in Raymond M. Smullyan's Satan, Cantor and Infinity
1
๐ฎ
๐๐ยท
I now have a somewhat general "pigeonhole solver" which, given a set of equations of the form x_iยฌ=x_j and for each x_i, one equation of the form x_iโ{c_j c_(j+1)
โ
c_(j+2) ... c_(j+k)}. This can directly be solved with a search, but I've been trying to avoid that in my pretense toward symbolic manipulation. In the end, I'm not
โฐ
sure my approach is all that different than a search - if I can write my approach up in a sensible form, I'll post a doc someplace and hope to learn more.