Re: Universal grammar

In article <874pttiv7x.fsf@xxxxxx>, Markus Triska <triska@xxxxxx> wrote:

where A(x) is a predicate. These are combined with axioms (medelson, p.57):
(K4) all x A(x) => A(t) if t is a term free for x in A.
(Gen) A |- all x A(x). (Generalization)

(Re-)introducing universal quantifiers is unnecsseary if you know that
you'll be using (a variant of) resolution (in Prolog: SLD-resolution),
since they are dropped again anyways after skolemization.

I decided to avoid such simplifications for various reasons. One is to
preserve (human intended) structure of formulas. Another, Skolem normal
form only applies to first order theories, and the existential quantifiers
appear before the universal quantifiers. In a axiomatic set theory, the
rewriting involves the axiom of choice.

And, as for Selected Literal Definite clause resolution, the Wikipedia
says it only applies to Horn clauses. - My resolution engine does
not operate on Horn clauses at all anymore, but only on the proof trees.

--
Hans Aberg
.

Relevant Pages

  • Re: Existential, Universal Quantifiers, Generalized Booleans
    ... existential and universal quantifiers. ... They warn that the generalization DeMorgan's Laws only ... The idea of specifying the domain in the underscript was just a lark. ... Either FireFox or Mozilla should work. ...
    (sci.math)
  • Re: Existential, Universal Quantifiers, Generalize Booleans
    ... backwards E used in all the English language math texts I have see using ... existential and universal quantifiers. ... They warn that the generalization DeMorgan's Laws ... indicates that it appears not to be in common use anywhere. ...
    (sci.math)
  • Re: Existential, Universal Quantifiers, Generalize Booleans
    ... backwards E used in all the English language math texts I have see using ... existential and universal quantifiers. ... They warn that the generalization DeMorgan's Laws only ... If you say that Ax Pis not an "infinite conjunction", ...
    (sci.math)
Quantcast