[SCL] implementing a nonstandard unifier

[pat hayes]

Greetings.  I would like to ask your opinion, as someone who has 
implementation experience with high-performance theorem-provers.

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.

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? 
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.

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.

Feel free to forward this message, and the request, to anyone you 
think may have a useful opinion to offer.

Thank you for your help.

Pat Hayes
-- 
---------------------------------------------------------------------
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