Spock: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
Spock is an XO activity and pygtk application that implements a simple text editor with | Spock is an XO activity and pygtk application that implements a simple text editor with | ||
an embedded proof verifier. The proof verifier is based on the | an embedded proof verifier. The proof verifier is based on (an older version of) the | ||
[http://sites.google.com/a/ghilbert.org/ghilbert/home Ghilbert] proof language, | [http://sites.google.com/a/ghilbert.org/ghilbert/home Ghilbert] proof language, | ||
with some modest extensions. Ghilbert in turn is inspired by the | with some modest extensions. Ghilbert in turn is inspired by the | ||
Latest revision as of 14:06, 28 February 2010
Spock is an XO activity and pygtk application that implements a simple text editor with an embedded proof verifier. The proof verifier is based on (an older version of) the Ghilbert proof language, with some modest extensions. Ghilbert in turn is inspired by the Metamath project. Spock, Ghilbert, and Metamath can express a wide variety of logics and theories.
The activity could be used as the basis for a course on elementary propositional or predicate logic (or even set theory), however as yet very little work has been done to make the activity friendly to children, and introductory materials are not yet available.
The code is hosted at [1].