Re: Many-sorted (or typed) logic
>>>>> pat hayes <phayes@ai.uwf.edu> writes:
[nice exposition deleted]
> Now it is not hard to tweak the syntax of the logical language to
> allow quantifiers over properties (and relations: again I won't
> bother with the details). You just allow variables to be put in the
> predicate position of an expression, ie you allow things like (?P a
> ?x) as well as (P ?x ?y), and then you allow them to be quantified.
> Nothing to it: CYCL does it without even batting an eyelid. (KIF
> carefully excludes this, which IMHO is a major problem for using KIF
> in ontology specification.
Just a minor addition: KIF 3.0 (not the stripped-down KIF proposed as
an ANSI standard) DOES allow second-order quantification via the
`holds' predicate (which is defined via the primitive `member'
relation). For example, the Ontolingua Frame Ontology uses `holds' to
define the transitivity property like this (all variables are
implicitly universally quantified):
(<=> (Transitive-Relation ?R)
(and (Binary-Relation ?R)
(=> (and (Holds ?R ?X ?Y)
(Holds ?R ?Y ?Z))
(Holds ?R ?X ?Z))))
Since you are working on a "CYClified version of KIF", you might want to
consider this notation, since it already has seen extensive/some :-)
use in various communities. The only restriction for ?R is that it
has to be a bounded relation (the specification of KIF 3.0 uses the
notion of bounded sets and objects to avoid Russel's paradox). Not
sure how this relates to your three choices of second-order universes.
Pragmatically, I don't think the choice matters much, since every
inference engine expected to deliver results during the lifetime of
its users will need to restrict reasoning with higher-order
constructs, which in turn might effectively implement some of the more
restrictive choices such as your #3. For example, a pragmatically
sensible application of the above rule would be to run it forward and
instantiate the transitivity rule for a specific relation `foo' (but
usually not to prove `(Transitive-Relation ?R)' by going the other
way). Advertisement: This is what PowerLoom does.
Used in this form, the higher-order construct is really just a
convenient way to represent an axiom schema, that could (in many
cases) be replaced by a macro mechanism outside of the language
without losing much.
Hans
------------------------------------------------------------------------------
Hans Chalupsky USC Information Sciences Institute
<hans@isi.edu> 4676 Admiralty Way
(310) 448-8745 Marina del Rey, CA 90292
------------------------------------------------------------------------------