[SCL] Re: implementing a nonstandard unifier

[pat hayes]

Thanks for your rapid reply.

>  > A number of us are considering drafting a logic standard with an
>>  extended syntax for FO logic in which relations and functions in
>>  atomic sentences are allowed to be arbitrary terms (including
>>  variables) rather than being required to be constants.  In all other
>>  respects the language is first-order, so the appropriate notion of
>>  unification in this logic would be similar to the usual FO unifier
>>  except that the unification algorithm would apply recursively to
>>  terms in the relation or function position (first) in an atom or term
>>  just as it does to terms in the other positions.
>
>It is a bit off line but unification is not the most important operation
>in the implementation, and definitely not a bottleneck in theorem
>provers performance. Indexing will suffer most (you mention this below).
>
>>  Obviously this can be mapped into conventional FO syntax by
>>  interposing a 'dummy' function or relation name in the front of each
>>  atom or term with a given arity; my question, however, is what would
>>  be the costs of implementing such a unification algorithm directly?
>
>If I remember the full story (you probably refer to KIF

Son of KIF, as it were, currently labelled SCL.

>), you probably
>speak about logic with equality. Then you get strange effects like
>
>   (!x)(!y)(x = y) -> (p <-> q)

The current semantics does not have these unusual properties. The 
conventional-syntax subset of the extended syntax has the usual 
meaning, unchanged from conventional FOL, hence the interest in 
preserving the form of current FOL axiomatizations while extending 
the inference machinery.

>The cost of implementing unification and other algorithms would probably
>be not so high, but if you have a large knowledge base with many atoms
>using a variable relation x(t1,..,tn), you are in trouble. Roughly
>speaking, because too many terms become unifiable.

True, but they would be so unifiable if uniformly translated into 
conventional FOL syntax using 'holds'. But I take your point that 
this notation might change the search dynamics in new ways.

>  > In your implementation experience, would your implementation style
>>  need to be radically modified if atoms and terms could have
>>  non-constant terms in the relation or function position? I have in
>>  mind such matters as indexing or hash-coding schemes which depend on
>>  relation or function name tables, for example, or optimizing
>>  call-outs to special code for handling particular cases such as
>>  transitive or reflexive relations. It would be particularly helpful
>>  if you could identify (or simply report on the existence of) any such
>>  problems which would *not* arise if the 'dummy function/relation'
>>  style were adopted, bearing in mind that this would produce axiom
>>  sets using only a very small number of relation and function symbols.
>
>If you want to build in a small number of particular variable-relation
>axioms, this can be done in many ways, depending on the axioms you
>have. For example, you can add additional rules to the resolution system
>as soon as statements such as transitive(p) occur.
>
>In general, architectures of modern provers are VERY complex and any
>additions like those you mentioned would be highly time-consuming.

Do you mean, for the programmers, or that they would slow down the 
operation of the code?

>
>>  I realize that to answer an open-ended technical question is a burden
>>  on your time, but if you were able to give even a short answer I
>>  would be grateful, as it may influence our decisions on writing what
>>  we hope will be a useful draft of a standards document for a logical
>>  notation.
>
>I would simply suggest to use a dummy predicate with a special meaning
>(e.g. holds) when you use non-constant relations. For example:
>
>   transitive(u) <->
>   (!x)(!y)(!z)(holds(u,x,y) & holds(u,y,z) -> holds(u,z,x))
>
>Of course in the logic holds will have a special semantics.
>
>Any other syntax that comes to my mind would be quite confusing.

It is quite popular with 'users' who write ontologies, hence our 
interest in supporting it if possible.

>Of
>course, it would be best to use a clearly visible name for this
>predicate, e.g. #holds.

Quite. It will be a logically reserved vocabulary. Thanks again for your input.

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 ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu   for spam