[SCL] some 'standard' contextual ontologies

[pat hayes]

Further to the previous message, here are a few possible 'standard' 
outer ontologies suitable for importing.  John, you might like #2: 
consider it as a present ;-)

1. Simple FOL

<scl:FOL>[[
(forall (?x)(not (and (Rel ?x) (Ind ?x)))) ;; nothing is both an 
individual and a relation;
Fun(Arity) ;; relations and functions have a single arity;
;; as well as importing this ontology, a first-order context should 
declare all relation, function;
;; and individual constants and should provide explicit arities for 
all named relation and ;
;; functions.  Note that the arity of a function includes the value. ;
]]

2. Lists of arguments

<scl:arglists>[[
;; scl:list relates LISP-style lists (a.k.a. RDF collections) to SCL 
argument sequences;
;; the first argument of the relation (value of the function) is a 
list; the remaining arguments;
;; are the elements of the list in head-tail order. ;
;; When used as a function, scl:list is analogous to LISP 'list', so 
is variadic. To restrict ;
;; oneself to a fixed-arity vocabulary, use only scl:cons and scl:nil. ;

(Fun scl:list scl:cons scl:hd scl:tl)
(scl:list scl:nil)
(forall (?x ?z)(iff (scl:list ?x @y) (scl:list (scl:cons ?z ?x) ?z @y) ))
;;converts between finite lists written as sequences and as cons/nil 
Sexpressions;
(forall (?x ?y ?z)(iff (= ?z (scl:cons ?x ?y) ) (and (= ?x (scl:hd 
?z)) (= ?y (scl:tl ?z)))))
;;defines head and tail on cons lists;
(forall (?r)(iff (?r @l) (?r (scl:list @l))
;; converts between SCL atoms and unary predications of argument lists;
(= 3 (Arity scl:cons)) ;; binary function has arity 3;
(= 2 (Arity scl:hd))
(= 2 (Arity scl:tl))
]]

Any ontology defined in the above context can write any atomic 
sentence optionally as a unary predication of a list written 
explicitly using scl:cons and scl:nil, and can quantify over lists in 
tail position to achieve the same effective expressiveness (more??) 
as SCL sequence variables, in a more conventional FO notation.

Note, if an ontology already uses lists for other purposes then this 
context might create unintended models; users should therefore use 
the scl:arglist vocabulary only for this purpose. It would also be 
acceptable to define an alternative context ontology on this pattern 
but using a proprietary terminology for argument lists, in order to 
distinguish them from SCL lists; but such an option might limit 
interoperability.

Note also that this context does require that models of the defined 
(inner) ontology admits lists into the universe of discourse. There 
is no way to avoid this while using a function as a list constructor, 
and no way to avoid that without adding some new syntactic forms to 
the language (which would go beyond what can be done in an SCL 
context ontology.)

2a. First-order with list arguments

<scl:FOLarglists>[[
(import scl:FOL)
(import scl:arglists)
;; Warning: in the inner ontology, any uses of scl:list with 
different numbers of arguments will produce;
;; a syntactic inconsistency;
]]

3. RDF notation for argument lists, if required:

<scl:argRDFcollections>[[
(import scl:arglists)
(= scl:hd rdf:first)
(= scl:tl rdf:rest)
(= scl:nil rdf:nil)
]]

This is similar to 2 but allows the use of the RDF collection 
vocabulary in addition to, or instead of, the SCL list vocabulary. 
RDF does not use an explicit cons function, but instead asserts that 
lists exist with a given head and tail. The conversion to the 
Sexpression form follows from the 'iff' in the hd/tl definition axiom.

Pat
-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes