This looks great!
This is the kind of things Norm would have announced on the "Recent news
items <http://us2.metamath.org/mpeuni/mmrecent.html>" section of the web
pages.
_
Thierry
On 14/12/2021 10:19, David A. Wheeler wrote:
Cool! Thanks for posting!
I suggest including in the README an example of how to invoke it (and maybe a
sample response).
Here's one that worked for me:
./completeness foo '( ph <-> ph )'
foo $p |- ( ph <-> ph ) $= wph wn wph wph wb wi wph wph wb wph wn wph wph wi
wph wph wi wn wi wn wi wph wn wph wph wb wi wph wn wph wph wi wn wn wi wph wn wph wph
wi wph wph wi wn wi wn wi wph wn wph wph wi wi wph wn wph wph wi wn wn wi wph wph
pm2.21 wph wph wi wph wph wi wn wn wi wph wn wph wph wi wi wph wn wph wph wi wn wn wi
wi wph wph wi notnot wph wph wi wph wph wi wn wn wph wn imim2 ax-mp ax-mp wph wn wph
wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wph wn wph wph wi wn wn wi wph wn
wph wph wi wph wph wi wn wi wn wi wi wph wn wph wph wi wi wph wn wph wph wi wn wn wph
wph wi wph wph wi wn wi wn wi wi wph wph pm2.21 wph wph wi wph wph wi wn wn wph wph
wi wph wph wi wn wi wn wi wi wph wn wph wph wi wi wph wn wph wph wi wn wn wph wph wi
wph wph wi wn wi wn wi wi wi wph wph wi wph wph wi wn mth8 wph wph wi wph wph wi wn
wn wph wph wi wph wph wi wn wi wn wi wph wn imim2 ax-mp ax-mp wph wn wph wph wi wn wn
wph wph wi wph wph wi wn wi wn ax-2 ax-mp ax-mp wph wph wi wph wph wi wn wi wn wph
wph wb wi wph wn wph wph wi wph wph wi wn wi wn wi wph wn wph wph wb wi wi wph wph wb
wph wph wi wph wph wi wn wi wn wb wph wph wi wph wph wi wn wi wn wph wph wb wi wph
wph dfbi1 wph wph wb wph wph wi wph wph wi wn wi wn biimpr ax-mp wph wph wi wph wph
wi wn wi wn wph wph wb wph wn imim2 ax-mp ax-mp wph wph wph wb wi wph wn wph wph wb
wi wph wph wb wi wph wph wph wi wph wph wi wn wi wn wi wph wph wph wb wi wph wph wph
wi wn wn wi wph wph wph wi wph wph wi wn wi wn wi wph wph wph wi wi wph wph wph wi wn
wn wi wph wph ax-1 wph wph wi wph wph wi wn wn wi wph wph wph wi wi wph wph wph wi wn
wn wi wi wph wph wi notnot wph wph wi wph wph wi wn wn wph imim2 ax-mp ax-mp wph wph
wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wph wph wph wi wn wn wi wph wph wph
wi wph wph wi wn wi wn wi wi wph wph wph wi wi wph wph wph wi wn wn wph wph wi wph
wph wi wn wi wn wi wi wph wph ax-1 wph wph wi wph wph wi wn wn wph wph wi wph wph wi
wn wi wn wi wi wph wph wph wi wi wph wph wph wi wn wn wph wph wi wph wph wi wn wi wn
wi wi wi wph wph wi wph wph wi wn mth8 wph wph wi wph wph wi wn wn wph wph wi wph wph
wi wn wi wn wi wph imim2 ax-mp ax-mp wph wph wph wi wn wn wph wph wi wph wph wi wn wi
wn ax-2 ax-mp ax-mp wph wph wi wph wph wi wn wi wn wph wph wb wi wph wph wph wi wph
wph wi wn wi wn wi wph wph wph wb wi wi wph wph wb wph wph wi wph wph wi wn wi wn wb
wph wph wi wph wph wi wn wi wn wph wph wb wi wph wph dfbi1 wph wph wb wph wph wi wph
wph wi wn wi wn biimpr ax-mp wph wph wi wph wph wi wn wi wn wph wph wb wph imim2
ax-mp ax-mp wph wph wph wb pm2.61 ax-mp ax-mp $.
I believe the minimized Metamath proof would be a lot smaller :-).
--- David A. Wheeler
On Dec 13, 2021, at 8:28 PM, Scott Fenton<[email protected]> wrote:
Hi all,
Some time ago, I wrote a script implementing the completeness theorem for
propositional calculus in the form of a tautology prover for Metamath. I just
uploaded it to Github. You can find it athttps://github.com/sctfn/completeness.
To use the script to prove biid, you would call "./completeness biid '( ph <-> ph )'".
This will produce an uncompressed $p statement that you can incorporate into set.mm. Furthermore, if
called with the "-d" flag, the script will instead produce a D-rule proof of the theorem.
Let me know what you think!
-Scott
--
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
[email protected].
To view this discussion on the web
visithttps://groups.google.com/d/msgid/metamath/CACKrHR87Hjhw7Zx4cVEX8eyig3UeQ%2B9r1KSQpr0vLORUKFDUeA%40mail.gmail.com.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/7f68b9f1-f863-f4a0-27bb-5f2406ffd70d%40gmx.net.
