[ATCH99] Algorithms and Theory of Computation Handbook, Mikhail J. Atallah, ed., CRC Press LLC, 1999.
raph: web-based proof assistants, some random comments:
- I think the OBJ3 suggestion is interesting, but I don't think it is something you need to get right straightaway: I would say it was a version 2 sort of issue. What it offers is a way of modularising axiomatic frameworks in a way that gives inheritance, so that the group axiomatisiation can inherit from the monoid axiomatisiation. Drawbacks: it involves category theory, nontrivial implementation, and you have to think carefully about namespace issues. Trying to figure out what basic axioms most peopl should use for the base theory is probably the best place to start.
- Since Nat <=> Nat x Nat we have the following are equivalent:
- One place predicates over Nat;
- Sets of Nat;
- Sets of Nat x Nat;
- Two place relations over Nat.
- One thing I'd like to see in a web-based proof assistant, is
some support for different classes of proof, with documentation,
so that a proof can have an quickly-checked for-machine proof, a well-documented research paper like proof (also machine checkable), and an elementary long-but-in-easy-steps didiactic proof, complete with URLs for background reading.