Hi, I am trying to convert First Order Predicate Logic (FOPL) sentences to sentences in Equational Logic (EL). I am using Skolem constants and function to represent FOPL existential quantification in the EL sentences. Here is an example of defining overlap in terms of the part-of relation:

-- FOPL definition of overlap \A denotes for all, \E denotes there exists ax [A9] : \A[x:Entity, y:Entity] \E[z:Entity] overlap(x, y) = (part-of(z, x) & part-of(z, y))

-- Equational logic (EL) definition of overlap -- In EL variables are univerally quantified, exestential quantification is simulated by Skolem function f. vars x y z : Entity eq [A9] : overlap(x, y) = (part-of(f(y), x) and part-of(f(x), y))

I have two questions: 1) Is the above translation valid? 2) Using this technique is it in general possible to represent FOPL sentences in EL.

Thanks, Pat