# First Order Logic (FOL) to Schematron

(Beta)

Derives ISO Schematron rules from FOL constraints.

NOTE: this target has been implemented within the OGC Testbed 11. The use case there was to derive ISO Schematron rules from AIXM business rules. The full process is described on the page Deriving Schematron from AIXM Business Rules, which includes a sample configuration as well.

# Conversion to ISO Schematron

For a valid FOL expression x, let τ(x) denote the equivalent XPath expression. The expression x may contain free variables (explicit or implicit), which need to be treated and bound to their definition context when computing τ(x).

The following table describes how all particular constructs of the First Order Logic language translate to XPath/Schematron.

NOTE: the derived ISO Schematron file uses ‘xslt2’ as queryBinding, which is based on an XSLT 2.0 implementation that supports XPath 2.0.

 First Order Logic construct (and category, if applicable) Textual representation (in log output) In words Schematron translation Universal quantification forall(t:x|p(t)) All members of some set x of objects or values shall fulfill predicate p. every τ(t) in τ(x) satisfies τ(p(τ(t)))where t translates to a unique \$ prefixed variable name, and τ(x) translates to current() if the quantification is at the outmost level. Existential quantification: „at least l and at most h” exists{l,h}(t:x|p(t)) The number of members of some set x of objects or values, which fulfill predicate p shall be between l and h. for \$var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return (\$var>=τ(l) and \$var<=τ(h)) Existential quantification: „exactly n” exists{n}(t:x|p(t)) The number of members of some set x of objects or values, which fulfill predicate p shall be exactly n. for \$var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return (\$var=n) Existential quantification: “at most n” exists{0..n}(t:x|p(t)) The number of members of some set x of objects or values, which fulfill predicate p shall be at most n. for \$var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return \$var<=n) Existential quantification: “at least n” exists{n..*}(t:x|p(t)) The number of members of some set x of objects or values, which fulfill predicate p shall be at least n. for \$var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return (\$var>=n) Variable access t defined in a quantification, such as forall(t:x|p(t)) the variable name, either explicitly or implicitly provided The variable name, preceded by ‘\$’ – for example \$x1, \$c1.Note: this is the translation for τ(t), which is mentioned in the Schematron translations of quantifications. Property call x.pname Set of object instances or values reached from the instance or set represented by x by applying property name, pname. If pname is encoded as an XML attribute:τ(x)/@pnameOtherwise, if pname is simple-valued or if pname is object-valued and the last segment in the schema call: τ(x)/pname Otherwise, if pname is object-valued and encoded inline: τ(x)/pname/* Otherwise, if pname is realized by reference using xlink:href pointing to object instances in the same document: //*[concat(α,@gml:id,β)= τ(x)/pname/@xlink:href] α and β are a prefix and a postfix to adjust xlink:href values and gml:ids. Typically bare name references are used – hence α=# and β=empty. Otherwise (if encoded inline or by reference): (τ(x)/pname/*)|//*[concat(α,@gml:id,β)= τ(x)/pname/@xlink:href] Logical infix and(x1,…,xn)or(x1,…,xn) Logical combination as indicated τ(x1) and … and τ(xn)τ(x1) or … or τ(xn) Negation not(x) Logical negation of x not(τ(x)) Null check isNull(x) Determine if the value of x is null. If the last segment of the patch expression in τ(x) is encoded as an XML attribute:not(string-length(normalize-space τ(x))))Otherwise: τ(x)[@xsi:nil=’true’] Equality isEqualTo(e1,e2) Equality of expressions e1, e2 τ(e1)= τ(e2)Note: This assumes that equality on sets is fulfilled if at least one pair is equal. Otherwise some more refined code generation will be necessary. Type check isTypeOf(x,(ClassLiteral)z) X is checked for complying with the type y identified by class literal z. τ(x)[name()=’T1‘ or … or name()=’Ti’], whereTk is the qualified name of one of the concrete derivations of y, including y, if it is not abstract (names of abstract types are ignored). String literal ‘xxxxx’ same Numeric literal 123 or 3.1415 same String literal list (‘abc’,’def’,…) List of ‘names’ same Class literal class name (e.g. AirportHeliport) name of the class name of the class identified by the class literal

# Configuration

## Class

The class for the Target implementation is de.interactive_instruments.ShapeChange.Target.FOL2Schematron.FOL2Schematron.

## Parameters

The <targetParameters> recognized for this target include the following:

 Parameter Name Required / Optional Type Default Value Explanation outputDirectory Optional String The path to the folder in which the Schematron rules file will be created. defaultEncodingRule Optional String none The identifier of the default encoding rule governing the conversion into Schematron. schematronXlinkHrefPrefix Optional String “#” Prefix for xlink:href references. schematronXlinkHrefPostfix Optional String “” (the empty string) Postfix for xlink:href references.

## Encoding Rules

An <EncodingRule> element defines an encoding rule.

Example:

```<EncodingRule extends="iso19136_2007" name="aixm">
<rule name="rule-all-cls-aixmDatatype" />
<rule name="rule-all-prop-uomAsAttribute" />
</EncodingRule>```

The name attribute of the <EncodingRule> element defines the identifier of the encoding rule to be used.

The optional extends attribute of the <EncodingRule> element includes all conversion rules from the referenced encoding rule in this encoding rule, too.

Each <rule> references either a conversion rule or – possibly in the future – a requirement or recommendation to be tested during the validation before the conversion process.

The following conversion rules are supported by this target. They amend or extend the default encoding behavior:

 Rule Name Description rule-all-cls-aixmDatatype A <> within an AIXM schema does not have its own object element. Within the XML Schema it only has a complex type with simple content definition containing a textual value (and possibly attribute(s)), but no element. rule-all-prop-uomAsAttribute When this rule is active, then the XML Schema encoding of a property with name “uom” is an XML attribute. The AIXM schema defines datatypes with such properties and encoding.

## Configuration Example

```<TargetXmlSchema class="de.interactive_instruments.ShapeChange.Target.FOL2Schematron.FOL2Schematron"
inputs="step3" mode="enabled">
<targetParameter name="outputDirectory" value="results/sch"/>
<targetParameter name="defaultEncodingRule" value="aixm"/>
<rules>
<EncodingRule extends="iso19136_2007" name="aixm">
<rule name="rule-all-cls-aixmDatatype"/>
<rule name="rule-all-prop-uomAsAttribute"/>
</EncodingRule>
</rules>
<xi:include href="src/main/resources/config/StandardRules.xml"/>
<xi:include href="src/main/resources/config/StandardNamespaces.xml"/>
<xi:include href="src/main/resources/config/StandardMapEntries.xml"/>
</TargetXmlSchema>```