Re: function symbols in SWRL FOL

On 25 Nov 2004, at 14:24, Sandro Hawke wrote:
>> Secondly, when we have equality (as we do in SWRL FOL), function 
>> symbols do not add to the expressive power of the language as we can 
>> easily substitute "functional" predicates. I was hoping to refer you 
>> to a suitable logic text book at this point, but one didn't 
>> immediately come to hand so I will attempt to DIY it. To make a 
>> predicate f "functional", we simply add:
> ...
>
> Can we characterize this transform in a few more regards?
>
> 1. The models of the pre-transform formula (F1) and the post-transform 
> formula (F2) are the same.

They are not. The transformation preserves the functionality, not the 
definition of the function. So, the models of F2 will be many more and 
will include the models of F1. So, functions symbols do increase the 
expressive power of the language.

> 2. It is lossy / not reversable. You can't look at F2 and figure out 
> what F1 must have been.

Yes, it is lossy.

> 3. For many computational logic systems, the performance 
> characteristics of operating with F1 will be significantly different 
> from those of operating with F2. (Where "significantly" is perhaps 
> extraneous, because theorem provers seem to be extremely sensitive to 
> syntactic transformations.

This is not clear. I suspect that since the encoding requires equality, 
there may be fragments of the logic in which it is more efficient to 
reason with built-in functions rather that equality - but this is just 
a guess.

> The other half of the puzzle is about the transform between n-ary 
> predicates and binary predicates (which I wish we could agree to call 
> dyadic predicates, since the word "binary" has such strong other 
> associations). There is a transform which effectively converts n-ary 
> to 2-ary predicates, but it is not perfectly model-preserving, since 
> it reifies the relationship.

Depending on the language (which shouldn't be too expressive), 
reification of n-ary relations may preserve satisfiability and logical 
implication, even if it does not preserve models (see, e.g., [1]).
So, there is a sense in which you can say that reification is not lossy.

[1] The Description Logic Handbook: Theory, Implementation and 
Applications. Cambridge University Press, 2002. Section 5.4.1 
("Reification of roles"), and Section 5.7 ("Relations of arbitrary 
arity").

cheers
--e.

Enrico Franconi                  - franconi@inf.unibz.it
Free University of Bozen-Bolzano - http://www.inf.unibz.it/~franconi/
Faculty of Computer Science      - Phone: (+39) 0471-016-120
I-39100 Bozen-Bolzano BZ, Italy  - Fax:   (+39) 0471-016-129

Received on Sunday, 5 December 2004 13:19:56 UTC