Re: [Metamath] Proof Design based on Natural Deduction

['Meta Kunt' via Metamath]

Natural deduction is so good, so so good. Context depth 1 makes everything work simply because you get free autocomplete.
I have a small list of theorems to use, so that if a certain problem pops up I know how to manipulate it in the right way.

I have made the point to even move all theorems from closed to deduction form, as the application of those would be much simpler. You get free autocompletes and unifications as the theorems are in a certain "normal form".
 

---

Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.

--
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+unsubscr...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/832db89be660297ae8660965bd194a2c%40mail.eclipso.de.