namespace dc = "http://purl.org/dc/elements/1.1/"
namespace dcterms = "http://purl.org/dc/terms/"
dcterms:title [ "RuleML Implications" ]
dcterms:identifier [ "http://deliberation.ruleml.org/1.02/relaxng/modules/implication_expansion_module.rnc" ]
dcterms:isPartOf [ "http://deliberation.ruleml.org/1.02/spec" ]
dcterms:creator [ "http://wiki.ruleml.org/index.php/User:Athant" ]
dc:subject [ "RuleML, implication" ]
dcterms:description [ "The expansion module for implications." ]
dcterms:language [ "en" ]
dc:rights [
'Copyright 2015 RuleML Inc. -- Licensed under the RuleML Specification License, Version 1.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at http://ruleml.org/licensing/RSL1.0-RuleML. Disclaimer: THIS SPECIFICATION IS PROVIDED "AS IS" AND ANY EXPRESSED OR IMPLIED WARRANTIES, ..., EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. See the License for the specifics governing permissions and limitations under the License.'
]
dcterms:rights [ "http://ruleml.org/licensing/RSL1.0-RuleML" ]
dcterms:relation [ "http://deliberation.ruleml.org" ]
start |= Implies.Node.def | head_Implies.edge.def | body_Implies.edge.def
Node.choice |= Implies.Node.def
edge.choice |= head_Implies.edge.def | body_Implies.edge.def
# This module declares the following RuleML elements and attributes:
# *
# *
# *
# This module also declares the following RuleML choice pattern:
# PremiseFormula.choice
# ConclusionFormula.choice
## a convenience pattern that unifies implications and equivalences
## because equivalence is allowed wherever implication is allowed.
Implication-node.choice |= Implies-node.choice | Equivalent-node.choice
# For the declaration of equivalences, see the equivalance module (equivalence_expansion_module)
## an extension point to allow alternate names and internationalization of uni-directional implication tag name.
Implies-node.choice |= Implies.Node.def
## An implication rule. It consists of a conclusion role () followed by a Premise role (), or, equivalently (since roles constitute unordered elements), a Premise role followed by a conclusion role.
## Alternatively, the roles may be skipped, in which case the Premise comes first followed by the conclusion as suggested by the element name 'Implies'.
## The children of the implication element are divided into two sections, a header section for modifiers, and a main section for the premises and conclusion.
Implies.Node.def =
## : an implication between two formulas, a premise and a conclusion. See
## http://deliberation.ruleml.org/1.02/glossary/#gloss-Implies
element Implies { Implies.type.def }
Implies.type.def = (Implies-datt.choice & reImplies.attlist), Implies.header, Implies.main
## Implications may have an optional closure attribute
## and will accept a scoped closure attribute at full first-order logic.
reImplies.attlist &= commonNode.attlist?
reImplies.attlist &= closure-att.choice?
reImplies.attlist &= mapClosure-att-fo.choice?
# For the declaration of the closure attribute pattern, see the quantification closure module (closure_expansion_module)
## Equations accept the header of truth-valued connectives
Implies.header &= TruthValuedConnective.header?
# For the declaration of the TruthValuedConnective header, see the modules ordered_groups_expansion_module and unordered_groups_expansion_module).
#
# Implies.main |= notAllowed is declared in the initialization module.
# This pattern must be over-ridden to allow the Implies element to be used.
# The pattern of the main content of an implication is serialization dependent,
# but it will contain exactly one if and one then.
# For the declaration of the main content of implications, see the serialization modules (orderstrict_module or orderlax_module)
##
## an extension point for stripe skipping as well as specializations of the if tag name in implications.
body_Implies.name.choice |= body_Implies.edge.def
## The if of an implication rule () containing the Premise(s), also known as the "antecedent" part of the rule.
## Also used as the "antecedent" part of an entailment ().
## Within Implies...
body_Implies.edge.def =
## : contains the premise of the implication. See
## http://deliberation.ruleml.org/1.02/glossary/#gloss-if
element if { body_Implies.type.def }
body_Implies.type.def = body_Implies.attlist? & body_Implies.content
body_Implies.attlist &= commonInit.attlist?
## The premise of an implication consists of a single formula
body_Implies.content |= PremiseFormula.choice
## formulas allowed to be premises.
PremiseFormula.choice |=
SimpleFormula-node.choice
| And-node.choice
| Or-node.choice
| Negation-node.choice
| NegationAsFailure-node.choice
| Implication-fo-node.choice
| Forall-fo-node.choice
| Exists-fo-node.choice
# For the declaration of the simple formula pattern, see the atomic formula module ( atom_expansion_module)
# For the declaration of conjunctive and disjunctive formula patterns, see the conjunction and disjunction module (andor_expansion_module)
# For the declaration of the strong negation formula pattern, see the strong negation module ( neg_expansion_module)
# For the declaration of the weak negation formula pattern, see the weak negation module ( naf_expansion_module)
# For the declaration of the implication pattern, see the implication modules (implication_expansion_module and equivalence_expansion_module)
# For the declaration of the quantification patterns, see the quantification module (quantifier_module)
## an extension point for stripe skipping as well as specializations of the then tag name in implications.
head_Implies.name.choice |= head_Implies.edge.def
## The then of an implication rule () containing the conclusion, also known as the "consequent" or "then" part of the rule.
## Also used as the "consequent" part of an entailment ().
## Within Implies...
head_Implies.edge.def =
## : contains the conclusion of the implication. See
## http://deliberation.ruleml.org/1.02/glossary/#gloss-then
element then { head_Implies.type.def }
head_Implies.type.def = head_Implies.attlist? & head_Implies.content
head_Implies.attlist &= commonInit.attlist?
## The conclusion of an implication consists of a single formula.
head_Implies.content |= ConclusionFormula.choice
## formulas allowed to be conclusions include atomic formulas.
ConclusionFormula.choice |=
Atom-head-node.choice
| Equal-head-node.choice
| And-head-node.choice
| Or-head-node.choice
| Negation-head-node.choice
| NegationAsFailure-node.notallowed
| Implication-head-node.choice
| Forall-head-node.choice
| Exists-head-node.choice
## backbone patterns
Atom-head-node.choice |= Atom-node.choice
Equal-head-node.choice |= Equal-node.choice
And-head-node.choice |= And-fo-node.choice
Or-head-node.choice |= Or-fo-node.choice
Negation-head-node.choice |= Negation-node.choice
Implication-head-node.choice |= Implication-fo-node.choice
Forall-head-node.choice |= Forall-fo-node.choice
Exists-head-node.choice |= Exists-fo-node.choice
# For the declaration of the simple formula pattern, see the atomic formula module ( atom_expansion_module)
# For the declaration of conjunctive and disjunctive formula patterns, see the conjunction and disjunction module (andor_expansion_module)
# For the declaration of the strong negation formula pattern, see the strong negation module ( neg_expansion_module)
# For the declaration of the weak negation formula pattern, see the weak negation module ( naf_expansion_module)
# For the declaration of the implication pattern, see the implication modules (implication_expansion_module and equivalence_expansion_module)
# For the declaration of the quantification patterns, see the quantification module (quantifier_module)