dmiles: The output can be a little anoying in that it defines a new operator "entails"
dajobe: Easier to read and understand
dmiles: "(forall (?x) (=> (p ?x) (q ?x)))"
dmiles: converts to:
dmiles: "(entails (not (q ?x)) (not (p ?x)))"
dmiles: "(entails (p ?x) (q ?x))"
dmiles: the form of (not (q ?x)) is virtually (q-not ?x)
dmiles: under this form, there are two universes positive and negative KB.. but a much better form will be in 4 universes form which will soon be put on page
dmiles: First 2 Universes - positive universally quantified literals,negative universally quantified literals
dmiles: Last 2 Universes - positive existentually quantified literals,negative existentually quantified literals
dmiles: In the last two, every variable that appears in literal can only be bound once
dajobe: Easier to read and understand
dmiles: "(forall (?x) (=> (p ?x) (q ?x)))"
dmiles: converts to:
dmiles: "(entails (not (q ?x)) (not (p ?x)))"
dmiles: "(entails (p ?x) (q ?x))"
dmiles: the form of (not (q ?x)) is virtually (q-not ?x)
dmiles: under this form, there are two universes positive and negative KB.. but a much better form will be in 4 universes form which will soon be put on page
dmiles: First 2 Universes - positive universally quantified literals,negative universally quantified literals
dmiles: Last 2 Universes - positive existentually quantified literals,negative existentually quantified literals
dmiles: In the last two, every variable that appears in literal can only be bound once
JosD__: looks very promising; propositional resolution; by dmiles
DanC: cf Propositional resolution
DanC: and the text book way to produce horn clauses from FOL, per dmiles
DanC: gotta noodle on this
DanC: also: discussion
DanC: and the text book way to produce horn clauses from FOL, per dmiles
DanC: gotta noodle on this
DanC: also: discussion
danbri: section 4.1. Fragment Identifier, "The semantics of a fragment identifier is a property of the data resulting from a retrieval action, regardless of the type of URI used in the reference."