[SCL] Re: implementing a nonstandard unifier

[Andrei Voronkov]

> 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), you probably
speak about logic with equality. Then you get strange effects like

  (!x)(!y)(x = y) -> (p <-> q)

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.

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

> 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. Of
course, it would be best to use a clearly visible name for this
predicate, e.g. #holds.

Best, AV