11
edits
Changes
Jump to navigation
Jump to search
Created page 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 [http://sites.google.com/a…'
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
[http://sites.google.com/a/ghilbert.org/ghilbert/home Ghilbert] proof language,
with some modest extensions. Ghilbert in turn is inspired by the
[http://www.metamath.org/ 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.
an embedded proof verifier. The proof verifier is based on the
[http://sites.google.com/a/ghilbert.org/ghilbert/home Ghilbert] proof language,
with some modest extensions. Ghilbert in turn is inspired by the
[http://www.metamath.org/ 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.