From: Yosi Scharf <syosi@MIT.EDU>

Date: Wed, 05 Jul 2006 16:18:37 -0400

Message-ID: <44AC1E9D.3050900@mit.edu>

To: public-cwm-talk@w3.org

CC: syosi@MIT.EDU

Date: Wed, 05 Jul 2006 16:18:37 -0400

Message-ID: <44AC1E9D.3050900@mit.edu>

To: public-cwm-talk@w3.org

CC: syosi@MIT.EDU

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

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 20:01:05 UTC
*