Spock: Difference between revisions
Jump to navigation
Jump to search
(New page: {{Translations}} == UNDER CONSTRUCTION == activity-spock.svg Spock is a new activity under development that will allow construction and verification of formal proofs. The proof lang...) |
|||
(One intermediate revision by the same user not shown) | |||
Line 3: | Line 3: | ||
== UNDER CONSTRUCTION == |
== UNDER CONSTRUCTION == |
||
[[ |
[[Image:Activity-spock.svg|Spock icon]] |
||
Spock is a new activity under development that will allow construction and verification of formal proofs. |
Spock is a new activity under development that will allow construction and verification of formal proofs. |
||
Line 10: | Line 10: | ||
ZFC set theory (based upon [http://metamath.org/ Metamath]). |
ZFC set theory (based upon [http://metamath.org/ Metamath]). |
||
Collaboration support and tutorial material will (eventually) be incorporated. |
Collaboration support and tutorial material will (eventually) be incorporated. |
||
Source code for the Spock activity is available [http://git.sugarlabs.org/projects/spock here]. |
Latest revision as of 21:03, 21 May 2010
Please copy/paste "{{Translationlist | xx | origlang=en | translated={{{translated}}}}}" (where xx is ISO 639 language code for your translation) to Spock/translations | HowTo [ID# 236246] +/- |
UNDER CONSTRUCTION
Spock is a new activity under development that will allow construction and verification of formal proofs. The proof language is based upon that of the Ghilbert proof verifier. Example axiom schema sets are provided for propositional logic, predicate logic with equality, and ZFC set theory (based upon Metamath). Collaboration support and tutorial material will (eventually) be incorporated.
Source code for the Spock activity is available here.