SUO: clausal normal form and skolemization

["Robert E. Kent" <rekent@ontologos.org>]

John et al,

 

Earlier today with reference to his message below, I had ask John Sowa for references to a "clear semantic" presentation for conversion to clausal normal form. After further consideration I believe the Skolemization involved may have problems of semantic and ontological relevance.

 

Any formula can be converted to clausal normal form automatically by:

1. Converting to Prenex form (all quantifiers appear at the beginning as a prefix).

2. Converting to conjunctive normal form (the body or matrix being a conjunction of disjunctions).

3. Converting to Skolem form (eliminating existential quantifiers by replacing existential variables with Skolem constants or Skolem functions of universal variables).

4. Eliminating universal quantifiers.

5. Separating conjunctions into clauses.

 

It is step 3 that seems somewhat problematic, since Skolem functions and constants are rather formal and involve an arbitrary choice. My question: Does Skolemization have a good semantic and ontological basis? Would the existential quantifiers, being replaced by Skolem functions in step 3, have been better modeled as "natural" functions; that is, functions with a good semantic sense? Any references that discuss this would be greatly appreciated.

 

Robert E. Kent

rekent@ontologos.org

----- Original Message -----
From: "John F. Sowa" <sowa@bestweb.net>
To: "Chris Menzel" <cmenzel@philebus.tamu.edu>; <martin_king@UK.IBM.COM>;
"IEEE Standard Upper Ontology List" <standard-upper-ontology@ieee.org>
Sent: Saturday, October 14, 2000 7:08 AM
Subject: Re: SUO: Re: Starter Ontology Version 2
...
> Gentzen showed that any arbitrary formula could be translated
> to a conjunction of "clauses", each of which has exactly one
> one implication, a conjunction of zero or more literals in the
> antecedent, and a disjunction of zero or more literals in the
> consequent.
...
> John Sowa