Cwm formula identity

I've been thinking about cwm logic recently, and reading things like
http://www.w3.org/DesignIssues/N3Logic . Further, I've been trying to code.

My assumptions on how the logic works appear in appendix A. I define
logical equivalence of two n3 formulae.

The question is, for n3 logic, when do we consider two formulae to be
equal? In particular, which of the following are legal / meaningful n3
statements?
1)    {@forAll :X . {:X a :Man} => {:X a :Mortal}. [ a :Man]} a log:Truth .
2)    {@forAll :X . {:X a :Man} => {:X a :Mortal}. [ a :Man]}
logTest:tripleCount 2 .
3)    {@forAll :X . {:X a :Man} => {:X a :Mortal}. [ a :Man]}
logTest:universalCount 1 .
4)    {@forAll :X . {:X a :Man} => {:X a :Mortal}. [ a :Man]}
logTest:existentialCount 1 .
5)    {@forAll :X . {:X a :Man} => {:X a :Mortal}. [ a :Man]}
log:universalVariableName  "http://example.com/#X" .
6)   {@forAll :X . {:X a :Man} => {:X a :Mortal}. [ a :Man]}
log:existentialVariableName 
"http://example.com/run_39084320943890583405#_g1".

In particular, note that the following are logically equivalent, yet if
we allow them equal only the first above is meaningful.
7) {@forAll :X . :X a :Duck. :Tim a :Duck}
8) {@forAll :Y . :Y a :Duck. :Yosi a :Duck}

There is nothing wrong with saying that. Note that we can define the
minimal form of an n3 graph, being that smallest graph logically
equivalent to it. The problem is that as far as I can tell, finding the
minimal form is equivalent to counting the number of ways it is
redundant, a #P complete problem. Even a proof the (7) is equivalent to
(8) is not quite as trivial as I would like --- the mappings of triples
each way is different.

It would be nice for equality to be easier to test. In particular, if we
could nail down the number of nodes in the graph, a graph isomorphism
algorithm would start becoming possible.

This needing a definition of equality happens all the time as we try to
match formula with quotes inside of them. When is it a legal match?

Yosi



Appendix A:
------------------------------
The following are truth preserving operations, which cannot make a
formula false:
    removing a triple
    adding a new triple made by replacing all instances of a variable in
a triple with anything
    replacing all instances of a node in a subset of the triples with a
new existential
    declaring a never used variable or existential
    removing the declaration of a never used variable or existential

A formula F implies G if a series of truth preserving operations go from
F to G
F and G are logically equivalent if both imply each other.

Received on Wednesday, 5 July 2006 20:18:54 UTC