[Top] [All Lists]

Re: [ontac-forum] RE: ontac-forum Digest, Vol 13, Issue 2

To: ONTAC-WG General Discussion <ontac-forum@xxxxxxxxxxxxxx>
From: Chris Menzel <cmenzel@xxxxxxxx>
Date: Wed, 17 May 2006 01:57:23 -0500
Message-id: <20060517065723.GS77713@xxxxxxxx>
On Wed, May 17, 2006 at 02:25:42PM +1200, Catherine Legg wrote:
> ..."in a logic-based representation the predicates and functions, their
> arities and their types, may all need to change during the course of
> reasoning...."
> I just want to say - as someone who did hands-on work in a logic-based
> representation for 2 years - how on earth is this to be effected? Could
> John or anyone else give me just a tiny operational clue?     (01)

How about a fully realized logical framework?  :-)  It is the default
for the languages (or "dialects") of Common Logic -- to whose
development John has been a major contributor -- that predicates and
function symbols denote relations and functions that do not have a fixed
arity.  (The predicates and function symbols can therefore take varying
numbers of terms as arguments.)  Granted, arity-freedom isn't quite the
same as fixed arities *changing*, as suggested in the quote above, but
the effect of the latter could be simulated via the former simply by
having axioms that determine the logical behavior of the same arity-free
predicate with respect to varying numbers of arguments.    (02)

CL languages are also (typcially) type-free, in that predicates and
function symbols can occur as arguments to other predicates and function
symbols.  (In fact, "predicate" and "function symbol" aren't even
genuine syntactic categories in CL, they are simply syntactic roles in
complex expressions; there is only a single class of "names" -- another
"web-centric" feature of CL that is actually a generalization of RDF
syntax in which the same URI can occur as subject, predicate, or object
in a triple.)  Despite some syntactic features typically associated with
second-order logic, Common Logic (at least, the variety lackign what KIF
called "sequence variables") is fully first-order and has a complete
proof theory.  The ISO Final Committee Draft of the CL spec can be found
at http://cl.tamu.edu .  The document is a technical spec, but it's
written in a fairly friendly, semi-formal way, and contains a good bit
of discussion.    (03)

Chris Menzel    (04)

Message Archives: http://colab.cim3.net/forum/ontac-forum/
To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki: 
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG    (05)
<Prev in Thread] Current Thread [Next in Thread>