Loading...
Please wait, while we are loading the content...
Similar Documents
The Circumscription of Existent Ial Formulae
| Content Provider | Semantic Scholar |
|---|---|
| Abstract | Let 4(P) be a first-order or a second-order formula with equality, involving the sequence P = (Pi,. .. , Ph) of predicate symbols and possibly other predicate symbols from a fixed underlying vocabulary u. Following McCarthy [McC80, McC86] and Lifschitz [Li85], we define the cir-cumscription ofP in 4(P) to be the following second-order formula 4*(P): 4(P) A ('dP')[(P' < w + ~w% where P' = (Pi,. .. , Pi) is a sequence of predicates and P' < P means that Pi c Pi, 1 2 i < k, and there is a j 5 E such that Pi is a proper subset of Pj. Several interesting cases have been pointed out in the recent past, in which the circumscription of a first-order formula collapses to a first-order formula. Lifschitz [Li85] showed that this holds for the class of separable formula.e, a natural and fairly wide class that includes all quantifier-free formulae. Such results, reducing the logical complexity of circumscription from second-order to first-order, are potentially valuable, in view of the intractability of second-order logic on the one hand and the completeness theorem for first-order logic on the other. We show below that the same holds for all exktential formulae. Theorem 1. Suppose that d(P) is an existential first-order sentence of the form 3x$, where x = (xi,. ..x~) is a sequence of variables and $ is quantifier-free formula. Then the circumscription qS+(P) of P in #(P) is equivalent to a first-order formula. 0 The proof of Theorem 1 constructs a first-order formula equivalent to the circumscription. We start by bringing $ in its complete disjunctive normal form, that is, $ is written as the disjunction of several formulae Bi, where each Bi is the conjunction of literals, where a literal can be either an atomic formula, or its negation, or an equality between two variables, or an inequality (#) between two variables; moreover, 'each disju.nct contains at least one of the literals xi = Xj or xi #.-Xj for any two variables xi, xj (that is, it determines an equality type). Next, we distribute the existential quantifiers over the disjunc-tion, and thus we have to show that each disjunct of the form 3~6iA('v'P')[(P < P),-+-(V~=, 3xoj)] is first order. However, since only existential. quantifiers occur in this dis-junct and Bi has a fixed equality type (in other words, the mapping from variables to constants is fixed up to renam-ings), the … |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.aaai.org/Papers/AAAI/1988/AAAI88-082.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
