# Reasoning Semantic Profile of RuleML 1.02

From RuleML Wiki

- Identifier: http://ruleml.org/1.02/profiles/reasoning
- Consequence Relation
- The logic must support a consequence relation satisfying Cautious Monotony, Cut and Reflexivity
^{[1]}.

- The logic must support a consequence relation satisfying Cautious Monotony, Cut and Reflexivity
- Laws of Deduction:
- Laws of deduction supported by the logic must satisfy the following properties. The properties apply to RuleML elements (in the namespace http://ruleml.org/spec) as specified below, and also to such elements decorated with unqualified attributes and child elements in the RuleML namespace, provided these attributes and elements are declared as
*annotational*in the glossary of the appropriate specification. The inferences from premises with attributes may not be assumed to inherit these attributes. The properties are stated in terms of XML fragments in the normalized serialization, but also apply to any set of XML fragments that would be mapped to these by the official normalizer XSLT transformation. - The laws are stated in a nontraditional form in order to allow the greatest flexibility in accommodating non-monotonic (esp. non-reflexive), as well as monotonic, logics. The law template is as follows:
- If Q is inferred from theory G union S, then Q is inferred from theory G union T, where G is an arbitrary set of logical formulas, Q is an arbitrary logical formula, and S, T are sets of logical formulas of a specified form.

- In the case that the semantics is reflexive, the law premises would be satisfied if Q is a member of S and G is the empty set. If the law premises are satisfied in this way, then the law conclusion holds and therefore T entails S, which is the traditional form of these laws.
- In all of the following laws, G is an arbitrary set of logical formulas.

- Simplification of Conjunction (Conjunction Elimination), modified for variably polyadic conjunction:
- Let P and Q denote logical formulas and ... denote a sequence of zero or more logical formulas enclosed in
`<formula>`

tags, with index values adjusted as necessary.

- If Q is inferred from {G, P,
`<And> ... </And>`

}, then Q is inferred from {G,`<And><formula index="1">P</formula> ... </And>`

}.

- Let P and Q denote logical formulas and ... denote a sequence of zero or more logical formulas enclosed in
- Conjunction Introduction, modified for polyadic conjunction:
- Let P and Q denote logical formulas, and ... denote a sequence of zero or more logical formulas enclosed in
`<formula>`

tags, with index values adjusted as necessary.

- If Q is inferred from {G,
`<And></And>`

}, then Q is inferred from G. - If Q is inferred from {G,
`<And><formula index="1">P</formula> ... </And>`

}, then Q is inferred from {G, P,`<And> ... </And>`

}.

- Let P and Q denote logical formulas, and ... denote a sequence of zero or more logical formulas enclosed in
- Modus Ponens:
- Let P, Q, and R denote logical formulas.

- If R is inferred from {G, P, Q}, then R is inferred from {G, P,
`<Implies><if>P</if><then>Q</then></Implies>`

}.

- Disjunction Introduction, modified for variably polyadic disjunction:
- Let P and Q denote logical formulas and ... denote a sequence of zero or more logical formulas enclosed in
`<formula>`

tags, with index values adjusted as necessary.

- If Q is inferred from {G,
`<Or><formula index="1">P</formula> ... </Or>`

} then Q is inferred from {G, P}. - If Q is inferred from {G,
`<Or><formula index="1">P</formula> ... </Or>`

}, then Q is inferred from {G,`<Or>... </Or>`

}.

- Let P and Q denote logical formulas and ... denote a sequence of zero or more logical formulas enclosed in
- Universal Elimination:
- Let P, Q denote logical formulas, c denote a ground term, and x denote a variable. P(c/x) denotes the result of replacing all free occurrences of x by c.

- If Q is inferred from {G, P(c/x)}, then Q is inferred from {G,
`<Forall><declare>x</declare><formula>P</formula></Forall>`

.

- Existential Introduction:
- Let P, Q denote logical formulas, c denote a ground term, and x denote a variable. P(c/x) denotes the result of replacing all free occurrences of x by c.

- If Q is inferred from {G,
`<Exists><declare>x</declare><formula>P</formula></Exists>`

}, then Q is inferred from {G, P(c/x)}.

- Substitution for Equivalence:
- Let P and Q denote logical formulas.

- Let I be the implication with P as premise and Q as conclusion:
`<Implies><if>P</if><then>Q</then></Implies>`

. - Let J be the implication with Q as premise and P as conclusion:
`<Implies><if>Q</if><then>P</then></Implies>`

. - Let C be the conjunction of I and J:
`<And><formula index="1">I</formula><formula index="2">J</formula></And>`

. - Let E be the equivalence with P and Q as arguments:
`<Equivalence><torso>P</torso><torso>Q</torso></Equivalence>`

. - Let A be a logical formula, and A(X/Y) be the logical formula denoting the result of replacing all occurrences of logical formula Y in A by logical formula X.
- If Q is inferred from {G, A(E/C)}, then Q is inferred from {G, A}.
- If Q is inferred from {G, A(C/E)}, then Q is inferred from {G, A}.

- Laws of deduction supported by the logic must satisfy the following properties. The properties apply to RuleML elements (in the namespace http://ruleml.org/spec) as specified below, and also to such elements decorated with unqualified attributes and child elements in the RuleML namespace, provided these attributes and elements are declared as
- Laws of Post-conditions: Assertions have no side-effects.
- Parent: Predefined Semantic Profiles of RuleML 1.02
- Example: http://deliberation.ruleml.org/1.02/exa/Datalog/datalog_style.ruleml