25 Oct 2002 chalst   » (Master)

Bram: The graph isomorphism problem in its general form is known to be NP-hard, this is a standard result. See, eg.:
[ATCH99] Algorithms and Theory of Computation Handbook, Mikhail J. Atallah, ed., CRC Press LLC, 1999.

raph: web-based proof assistants, some random comments:

  1. 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.
  2. 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.
    Since functions Nat => Nat are a subspace of the two place relations over Nat, and two place relations are isomorphic to the functions Nat x Nat => {0,1}, moving between the two representations for Z_2 is pretty trivial (with the right definitional framework).
  3. 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.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!