Spock: Difference between revisions

From OLPC
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...)
 
No edit summary
Line 3: Line 3:


== UNDER CONSTRUCTION ==
== UNDER CONSTRUCTION ==
[[activity-spock.svg]]
[[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.

Revision as of 18:51, 25 October 2008

  Please copy/paste "{{Translationlist | xx | origlang=en | translated={{{translated}}}}}" (where xx is ISO 639 language code for your translation) to Spock/translations HowTo [ID# 177200]  +/-  


UNDER CONSTRUCTION

Spock icon

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.