Positive Triples Logic

Status

$Revision: 1.4 $ $Date: 2002/06/24 16:55:17 $

A proposal, presented as a challenge on rdf-logic

Still drafty text and missing some sections, but the essential technical content is solid.

Background

I recently challenged people on this list to construct a paradox using a specific Turing-Complete subset of cwm/n3 logic [1], but I was unable to provide sufficient documentation for that logic. I also called the logic Horn-like, but Peter F. Patel-Schneider pointed out an important difference [2]. So I've coined a new name, which I think has the right connotations: "Positive Triples Logic". If anyone knows of an established name for this particular formalism, please let me know.

Introduction

This logic is terribly simple. The only thing that makes it complicated is encoding its syntax in RDF. To make this clear, I first introduce the logic with a simple, informal syntax, then propose two RDF encodings. The first I believe to be free of RDF logic layering problems. The second I believe to be plagued by them in several different ways; I include it to help clarify the discussion of those plagues. In particular, I'm wondering if Dark Triples would allow the second encoding to function properly.

Informal Syntax (n3x)

This syntax (call it n3x) is like n3 except

Blocks ( "{ ... }" constructs ) can only occur in a triple like this:
```
        { inblockn3 } @implies { inblockn3 }. 
```
Inblockn3 is just like regular n3 except
- it must not contain the block-implies-block constructions (no nesting)
- it may contain universally quantified variables like ?x
- it may contain existentially quantified variables like !y

The scope of quantification is implicit in the @implies construct; universally quantified variables ("univars") cover both blocks, existentially quantified variables ("exivars") cover a single block.

The construct

    { :x :y ?x } @implies { !c :p ?x.  !c :q ?x }.

means: for all ?x, if the triple ":x :y ?x" is true, then it must be true that there exists some !c such that both the triple "!c :p ?x" and the triple "!c :q ?x" are true.

This is similar to Horn clauses (familiar to Prolog programmers), but differs in a few ways:

there is no way to express or check for triples being known false
there is no way to express or check for triples not being known to be true
there are no logic functions

The lack of logic functions prevents us from eliminating exivars through Skolemization. In fact, if we want to express function-like information involving univars, we have to use exivars.

Exivars on the left of a @implies can be turned into univars with no effect; univars which occur only on the left of an @implies can be turned into @exivars with no effect. (Both of these changes only work, of course, if the new name is not already being used.)

Here's an example, saying "If someone has a grandfather, then they have a father whose father is their grandfather."

   { ?someone :grandfather ?grandfather } @implies
   { ?someone :father !father.  !father :father ?grandfather }

I believe a biconditional would be correct here, but we don't have one in this language, so we'll have to write it explicitely. "If someone has a father X, and X has a father Y, then the someone has a grandfather Y."

   { ?someone :father !father.  !father :father ?grandfather } @implies
   { ?someone :grandfather ?grandfather }

You could change "!father" to "?father" in that example with no change in meaning. (Perhaps it would reduce human error to say that univars are not allowed on the left side unless they also occur on the right side.)

I think this is the axiomatic semantics of rdfs:subClassOf:

 { ?instance rdf:type ?subclass.  ?subclass rdfs:subClassOf ?superclass }
 @implies { ?instance rdf:type ?superclass }.

RDF Encoding #1

We can parse an n3x file into an RDF graph if we specify what triples are added to encode each @implies construct. There are probably many ways to do this; here's a verbose one that I think will work. The encoding require 1 + 8 * NumberOfStatements triples.

The first grandfather example in RDF/XML.

The schema (ontology) is available in the original n3, translated to RDF/XML, or most properly subject to content negotiation.

PT1's axiomatic semantics in Otter's simple FOL dialect. With this we can use Otter to do PT inference (see demo), and use Mace to prove our axioms are satisfiable (see results). We need a few little wrappers to automatic this.

RDF Encoding #2 (Perhaps Deeply Flawed)

@@@@ to do

Is this Turing Complete?

My intuition as a programmer says it is. How should this be demonstrated? Defined the semantics (in PTL) of a predicate which maps between successive states of a universal Turing machine? Or of a virtual machine running any Turing complete language?

Sandro Hawke
First: 2002-03-29; This: $Id: Overview.html,v 1.4 2002/06/24 16:55:17 sandro Exp $