Talking About Computation
Well, I can talk about it, but I don't class this as thinking really.
See Magma (algebra) for a definition of groupoids.
See Magma - Computer Algebra System and https://prooftoys.org/ian-grant/hm/. And I have just learned something really interesting about prooftoys from a github repo where it is said that the proof assistant is based on an implementation (called Q0) of Church's Simple Theory of Types by Professor Peter Andrews (CMU Emeretus). You can read about the ETPS (Educational Theorem Proving System) in ETPS: A System to Help Students Write Formal Proofs.
Comments
Post a Comment