@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix daml: <http://www.daml.org/2001/03/daml+oil#>.
@prefix dc: <http://purl.org/dc/elements/1.1/>.
@prefix lx: <http://www.w3.org/2002/08/LX/RDF/v1#>.
@prefix rx: <http://www.w3.org/2002/05/rx/v1#>.
@prefix : <http://www.w3.org/2002/08/LX/RDF/v1#>.

<> daml:versionInfo "$Id: v1.n3,v 1.2 2002/08/29 19:33:56 sandro Exp $";
   dc:Author "Sandro Hawke sandro@w3.org";
   dc:Description """

       An encoding for LX sentences and their syntactic components
       into RDF triples.  Since LX is an extension of RDF, this can be
       used for RDF reification.

   """;
   rx:note """Obsoleted by 
   <a href="http://www.w3.org/2002/08/LX/RDF/v2">v2</a>""";
   rdfs:seeAlso <http://www.w3.org/2002/08/LX/RDF/v2>;
   rdfs:seeAlso <http://www.w3.org/2002/08/LX/RDF/layering>.

:Formula
    rx:name "Logic Formula";
    rx:superclass rdfs:Class;
    rx:cdef """A Triple or a Conjunction, Disjunction, Conditional,
    Biconditional, or Quantification whose subformulas are Formulas.""";
    rx:note """It's hard to find a good definition which is not
    inductive, build from these subclasses.  Maybe that's good
    enough.""".

:Sentence                     
    rx:name "Logic Sentence";
    rx:name "Closed Formula";
    rx:superclass :Formula;
    rx:cdef """A <a href="#Formula">Formula</a> with no free
    variables.""";
    rx:cdef """For us this means every <a href="#Term">Term</a> either
    has a <a href="#denotation">denotation<a/> or is
    is quantified (using a properly structured <a
    href="#Quantification">
    Quantification</a>.""".

:TrueSentence
    rx:name "True Sentence";
    rx:name "Assertion";
    rx:name "Truth";
    rx:superclass :Sentence;
    rx:cdef """A <a href="#Sentence">Sentence</a> which is as true as
    the RDF statement(s) being used to state (or imply) that this is a true
    sentence.  These may not contain negated syntactic loops.""";
    rx:note """The looping restriction, similar to KIF's wtr, makes
    the existence of a liar paradox statement ('this is false')
    forbidden.   @@@ link to discussion?""".

:FalseSentence
    rx:name "False Sentence";
    rx:name "Refutation";
    rx:name "Falsehood";
    rx:superclass :Sentence;
    rx:cdef """A <a href="#Sentence">Sentence</a> which is as untrue as
    the RDF statement(s) being used to state (or imply) that this is a true
    sentence.  These may not contain negated syntactic loops.""";
    rx:note """The looping restriction, similar to KIF's wtr, makes
    the existence of a liar paradox statement ('this is false')
    forbidden.   @@@ link to discussion?""".
	
:Triple
    rx:name "Triple";
    rx:name "RDF Atomic Formula";
    rx:superclass :Formula;
    rx:cdef """An atomic formula which implicitly uses the ternary "rdf"
    predicate to relate the things denoted by three terms: the <a
    href="#subject">subject</a>, <a href="#predicate">predicate</a>,
    and <a href="#drectObject">direct object</a>.""";
    rx:node """This is very similar to an <a
    href="http://www.w3.org/1999/02/22-rdf-syntax-ns#Statement"
    >rdf:Statement</a> but provides an additional a layer of
    indirection so we can easily distinguish terms (variables and
    constants) from the objects-in-the-domain-of-discourse which they
    denote.""".

:subjectTerm
    rdfs:domain :Triple;
    rdfs:range :Term.

:predicateTerm
    rdfs:domain :Triple;
    rdfs:range :Term.

:objectTerm
    rdfs:domain :Triple;
    rdfs:range :Term.

:SubformulaProperty
    rx:superclass daml:UniqueProperty;
    rx:cdef """A property relating formulas and their component
    subformulas or 'child' formulas"""; 
    rx:note """Should this be a class of properties, or should it be a
    property?   Let's try a class for now.""".
    
:Conjunction
    rx:superclass :Formula;
    rx:cdef """A formula whose truth value is the boolean "and" of the
    truth values of its left and right subformulas.  """.

:conjLeft
    rx:name "left subformula of conjunction";
    rx:name "both";	
    rx:superclass :subformulaProperty;
    rdfs:domain :Conjunction;
    rdfs:range :Formula.

:conjRight
    rx:name "right subformula of conjunction";
    rx:name "and";	
    rx:superclass :subformulaProperty;
    rdfs:domain :Conjunction;
    rdfs:range :Formula.

#  same for Disjunction/either/or
#  same for Conditional/if/then
#  same for Biconditional/iff/thenn
#  same for Negation/negated

:Quantification             
    rx:superclass :Formula;
    rx:cdef """A formula whose truth value depends on the truth value
    of its subformula after substition of its variable.""";
    rx:note """We don't distinguish between existential and universal
    quantification here; that distinction is a property of the
    variables themselves.  This is somewhat non-traditional, but I
    think it makes the formal semantics simpler.""".	

:variable
    a daml:UniqueProperty;
    rdfs:domain :Quantification;
    rdfs:range :Variable.

:subformula
    rx:superclass :subformulaProperty;
    rdfs:domain :Quantification;
    rdfs:range :Formula.

:Term 
    rx:superclass rdfs:Class;
    daml:disjointWith :Formula.

:denotation
    rdfs:domain :Constant;
    rdfs:range rdfs:Resource;
    rx:pdef """The thing (resource, object in domain of discourse) which
    is denoted by the subject.""".

:Constant
    rx:superclass :Term;
    daml:disjointWith :Variable.

:Variable
    rx:superclass :Term.

:UniVar
    rx:superclass :Variable;
    daml:disjointWith :ExiVar.

:ExiVar
    rx:superclass :Variable.




#########   Substructure (still unused) 

:uname
    a daml:UnambiguousProperty;
    rdfs:domain rdfs:Resource; 
    rdfs:range rdfs:Literal;
    rx:pdef """A string which identifies exactly one thing (the subject)""";
    rx:note """We normally use URI-References, but that's a special
    case of this""";
    rx:note """log:uri may not be the same; it's not subject to
    substitution.""" .

# do we use a property to link a Literal to its chars, or just
# say it's already a collection?    What about XML literals, and
# and language tagging?    Maybe I should steer clear of rdfs:Literal.
#
# -> use :zero, :succ, :unicode3 and rdf:List to build literals!