[SCL] Re: implementing a nonstandard unifier

[Stephan Schulz]

Hi Pat!

On Thu, Jun 05, 2003 at 07:21:07PM -0500, pat hayes wrote:
> 
> 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 mostly agree with what Andrei has said. Implementing the basic
unification algorithm would not be hard. Matching with indexing would
be slightly harder, but not too much. However, adding this to my
existing prover (and probably most C/C++ systems) would be quite
hard. E is build around a carefully designed the term data structure -
this is the hard of the prover. If I had to explicitely implement your
new terms, I would basically have to start at that level, and rebuild
most of the other code.

Also, I don't exactly know how term orderings can be extended to your
new scheme (in particular without loosing termination if you allow
essentially infinite function "symbol" sets). At least in E, I need
terminating simplification orderings, or very bad things may happen.

Some questions: Would the functional terms share the same signature as
the normal terms? The same variables? How would the concrete syntax
look?

Bye,

    Stephan
-- 
-------------------------- It can be done! ---------------------------------
   Please email me as schulz at informatik.tu-muenchen.de (Stephan Schulz)
----------------------------------------------------------------------------