Content Model for Negations

[greenTara]

The content model for the <strong> and <weak> edges in Neg and Naf, as well as the in Negation, are allowed to have any kind of negation (Neg, Naf or Negation).

This doesn't fit well with the Derivation RuleML backbone, which allows arbitrary compounding of Neg at the level of FOL, but still doesn't allow Naf inside of Neg or Naf even at FOL expressivity.

[greenTara]

For now, I have changed the driver schemas to override the definition of NegationFormula.choice when the strong negation module is included. Also, Negation-node.choice pattern is expanded to include all kinds of negations, allowing arbitrary compounding of all defined types of negation.

However, this needs to be developed differently in the next version, so that the restriction against Naf inside Neg is an option available to those who want it.

[apaschke]

Yes, with the expressiveness of RelaxNG a more fine grained configuration of the supported negation(s) becomes possible, with e.g. the following configuration choices, no negation (definite logic programs), negation as failure (normal logic programs), naf-neg (extended logic programs) and other negations using the generic Negation element (e.g. inflationary negation in production rules, negation in complex event detection).

[greenTara]

There is more to it than that. Deliberation RuleML has had negdatalog, nafdatalog and nafnegdatalog for awhile, in the XSD. However the compounding of the two types of negation was restricted.

• Below FOL, Neg could not be nested within Neg.
• At no level of expressivity could Naf be nested in Neg (or anything else, I believe.)

[apaschke]

Some of the the Reaction RuleML formalisms require the expressiveness of extended logic programs where Naf is nested in Neg to express that the contrary (neg) cannot be proven (naf). The semantics in Reaction RuleML is restricted by a coherence principle with the intuition that explicit Neg implies default Naf.

Extended logic programming expressiveness should be an extended choice in the Myng configuration. The standard is only one type of negation (strong or weak) or the polymorphic Negation where the intended semantics is defined by the default semantic profile.

[greenTara]

I'm going to close this issue on Github. I think we need to open this as a more general discussion on the wiki. It will definitely not be addressed in the 1.0 release.

[greenTara]

Adrian - I'm not very familiar with these various flavors of combining
negation, so I googled extended logic programming. I found this reference

http://www.doc.ic.ac.uk/~mjs/teaching/KnowledgeRep491/ExtendedLP_491-2x1.pdf

What I see here is that Naf ("not" in their notation) is always the
outer negation, and Neg (the sideways bracket-like thing) may be inside.
This is exactly what is allowed in nafnegdatalog in RuleML 1.0.

With the interpretation of Naf as "cannot be proved", this does
correspond to "the contrary of a literal P (Neg P) cannot be proved".

Whereas (Neg (Naf P) ) would be the contrary of "P cannot be proved",
and that seems to me to be something different. What am I missing?

Tara

On 3/28/14 3:49 PM, Adrian Paschke wrote:

Some of the the Reaction RuleML formalisms require the expressiveness
of extended logic programs where Naf is nested in Neg to express that
the contrary (neg) cannot be proven (naf). The semantics in Reaction
RuleML is restricted by a coherence principle with the intuition that
explicit Neg implies default Naf.

Extended logic programming expressiveness should be an extended choice
in the Myng configuration. The standard is only one type of negation
(strong or weak) or the polymorphic Negation where the intended
semantics is defined by the default semantic profile.

—
Reply to this email directly or view it on GitHub
#40 (comment).

[apaschke]

I looked it up in the RBSLA project where extended LPs are used. The nesting is naf-neg. So this is correct and Neg(Naf(.) should be disallowed.

[greenTara]

Do you want to make this change in the XSD at this stage, or postpone it to a later revision?

[greenTara]

I have updated the RNC content models of negation to match those in the XSD. There are still a few redefinitions needed for synchronization, but it is less than before.

Let's review these redefinitions in a Technical Telecon before closing this issue.

[greenTara]

One resolution from the review of the redefinitions is that there is a need for two kinds of Exists - one that allows Naf (whenever the Naf module is included) and one that does not. The first kind of Exists is new to Derivation RuleML - up until now, Exists was never allowed to contain Naf, even at FOL expressivity.

The following patterns in DR 1.0 reference Exists (I show only the Naf and Exists dependencies):

AndFormula.choice |= NegationAsFailure-node.choice | Exists-fo-node.choice
OrFormula.choice |= NegationAsFailure-node.choice | Exists-fo-node.choice
PremiseFormula.choice |= NegationAsFailure-node.choice  | Exists-fo-node.choice
ConclusionFormula.choice |= NegationAsFailure-node.notallowed  | Exists-fo-node.choice
NafFormula.choice |= NegationAsFailure-node.notallowed  | Exists-fo-node.choice
NegFormula.choice |= NegationAsFailure-node.notallowed  | Exists-fo-node.choice
AssertRetractFormula.choice |= NegationAsFailure-node.notallowed  | Exists-fo-node.choice
QueryFormula.choice |= NegationAsFailure-node.choice  | Exists-node.choice
ForallFormula.choice |=   | NegationAsFailure-node.notallowed   | Exists-fo-node.choice
ExistsFormula.choice |=  | NegationAsFailure-node.notallowed   | Exists-node.choice
RulebaseFormula.choice |= | NegationAsFailure-node.notallowed | Exists-fo-node.choice

In Reaction RuleML we also have (corrected):

AndQueryFormula.choice |=  | NegationAsFailure-node.choice  | Exists-fo-node.choice
OrQueryFormula.choice |=  | NegationAsFailure-node.choice  | Exists-fo-node.choice

and the problematic

ExistsFormula.choice |= NegationAsFailure-node.choice    | Exists-node.choice

If we now define two kinds of existentials:

Exists-Query-node.choice = element Exists{ ... ExistsFormulaQuery.choice}
  ExistsFormulaQuery.choice |= NegationAsFailure-node.choice    | Exists-Query-node.choice
Exists-node.choice = element Exists{ ... ExistsFormula.choice}
  ExistsFormula.choice |= NegationAsFailure-ae.choice    | Exists-node.choice

then we can also have (edited)

AndFormula.choice |= NegationAsFailure-node.choice | Exists-fo-node.choice
OrFormula.choice |= NegationAsFailure-node.choice | Exists-fo-node.choice
PremiseFormula.choice |= NegationAsFailure-node.choice | Exists-Query-node.choice
ConclusionFormula.choice |= NegationAsFailure-ae-node.choice | Exists-fo-node.choice
NafFormula.choice |= NegationAsFailure-ae.choice | Exists-fo-node.choice
NegFormula.choice |= NegationAsFailure-ae.choice | Exists-fo-node.choice
AssertRetractFormula.choice |= NegationAsFailure-ae-node.choice | Exists-fo-node.choice
QueryFormula.choice |= NegationAsFailure-node.choice | Exists-Query-node.choice
ForallFormula.choice |= | NegationAsFailure-ae-node.choice | Exists-fo-node.choice
RulebaseFormula.choice |= | NegationAsFailure-ae-node.choice | Exists-fo-node.choice
AndQueryFormula.choice |= | NegationAsFailure-node.choice | Exists-Query-fo-node.choice
OrQueryFormula.choice |= | NegationAsFailure-node.choice | Exists-Query-fo-node.choice

and the following changes in con/disjunction nesting

AndFormula.choice |= And-node.choice | Or-node.choice
OrFormula.choice |= And-node.choice | Or-node.choice
PremiseFormula.choice |= And-Query-node.choice | Or-Query-node.choice
ConclusionFormula.choice |= And-fo-node.choice  | Or-fo-node.choice
NafFormula.choice |= And-fo-node.choice | Or-fo-node.choice
NegFormula.choice |= And-fo-node.choice | Or-fo-node.choice
AssertRetractFormula.choice |= And-fo-node.choice | Or-fo-node.choice
QueryFormula.choice |= And-Query-node.choice  | Or-Query-node.choice
ForallFormula.choice |= | And-fo-node.choice | Or-fo-node.choice
ExistsFormula.choice |= | And-node.choice | Or-node.choice
RulebaseFormula.choice |= And-fo-node.choice | Or-fo-node.choice
AndQueryFormula.choice |= | And-Query-node.choice  | Or-Query-node.choice
OrQueryFormula.choice |= | And-Query-node.choice  | Or-Query-node.choice

This would partially maintain a dichotomy of compound formulas which can have Nafs within, and those that cannot. However, there will still be some mix-up at the level of FOL through Implies containing Naf in Premises. This use of Naf (in the body of Implies, compounded arbitrarily within other formulas, including Neg) is considered acceptable in the current Deliberation RuleML 1.0.

[greenTara]

From dr-flat.rnc we currently have

And.content =
meta-roles.content,
(element formula { formula-and-or.type }
| formula-and-or.content)*
And-query.type = And.content, And-query.attlist
And-inner.type = And.content, And-inner.attlist
This shows that in the XSD we have

AndQueryFormula.choice |= | And-node.choice | Or-node.choice
OrQueryFormula.choice |= | And-node.choice | Or-node.choice
rather than
AndQueryFormula.choice |= | And-Query-node.choice | Or-Query-node.choice
OrQueryFormula.choice |= | And-Query-node.choice | Or-Query-node.choice
as proposed above.
This is accommodated in two modules
drrr_andor_strict_expansion_module and drrr_andor_expansion_module, resp.

Similarly
if.content =
inner-connective.content | extended-signature-predicate-sorts.content
inner-connective.content =
element Operator { ConnectiveOperator.type }
| element And { And-inner.type }
| element Or { Or-inner.type }
| Negation
| Naf
| Neg
| Equal

corresponding to
PremiseFormula.choice |= And-node.choice | Or-node.choice
PremiseFormula.choice |= NegationAsFailure-node.choice | Exists-fo-node.choice

instead of
PremiseFormula.choice |= And-Query-node.choice | Or-Query-node.choice
PremiseFormula.choice |= NegationAsFailure-node.choice | Exists-Query-node.choice

This is accommodated in two modules
drrr_implication_content_strict_expansion_module and drrr_implication_content_expansion_module, resp.

Further dr-flat.rnc contains
then.content =
outer-connective.content | extended-signature-predicate-sorts.content
outer-connective.content =
element Operator { ConnectiveOperator.type }
| Negation
| Neg
| Equal
This is in agreement with the proposal above.

The content for the negation elements comes from
weak.content = formula-negation.content
strong.content = formula-negation.content
formula-negation.content =
element Operator { ConnectiveOperator.type }
| Equal
| Negation
| Neg
| extended-signature-predicate-sorts.content
So all three negation elements have the same content, which is consistent with the proposal above, assuming that Naf is not auto-epistemic (ae)
NegationAsFailure-ae-node.choice = notAllowed
This is implemented in the initialization module (init_expansion) and then activated in the ae module with
NegationAsFailure-ae-node.choice |= NegationAsFailure-node.choice

...still to verify
Query
Forall
Exists
Rulebase