[SCL] Re: implementing a nonstandard unifier

[Alexandre Riazanov]

On Fri, 6 Jun 2003, Andrei Voronkov wrote:

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

This is not much worse than 

(!x)(!y)(x = y) -> (!x1,..,xm)(!y1,..,yn)(f(x1,..,xm) = g(y1,..,yn))

in the standard FOL with equality.

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

This also applies to the solution using "holds/apply". 
You need to be able to specify special strategies to deal with 
axioms like transitive(p). Essentially, if you have a clause
~transitive(X) \/ C(X), you should probably first instantiate X
by resolving the literal ~transitive(X), because C(X) is too prolific.
But in this case you lose much of the benefits the new notation provides
(exept the succint notation, of course), since you 
will restore the transitivity axiom for all transitive predicates.
Optimising the kernel of an implementation like Vampire
for "holds/apply" must not be too difficult. Sorting out the strategies
seems to be the difficult part.


============================================================================
Alexandre Riazanov (Alexander Ryazanov)
Research Assistant, Computer Science Dept., University of Manchester,
tel : +44 161-2756132 
fax : +44 161 2756204 
email : riazanov at cs.man.ac.uk
home page URL: http://www.cs.man.ac.uk/~riazanoa
============================================================================