# RuleML Controlled Language

**Author:** Harold Boley
**RuleML Technical Memo**

RuleML Controlled Language (RCL) is proposed as an interface for RuleML, particularly for PSOA RuleML's logical presentation syntax, employing natural-language-like keyword syntax, specifically English-like, so it can be easily (a) used by domain experts and (b) mapped from and to RuleML syntax.
For representing the PSOA RuleML systematics of atoms, RCL employs keywords as follows: `a` (prefixing the predicate), `emptup` (denoting the empty tuple), `thru` (infixing any two final terms of a tuple), `plus` (infixing any two final descriptors, i.e. tuples or slots, of a descriptor sequence), `of` (prefixing any predicate-dependent descriptor sequence), `with` (prefixing any predicate-independent descriptor sequence), and `alongside` (infixing any two final `of`/`with`-prefixed descriptor sequences).
Descriptor sequences scoping the same dependency kind are a novel PSOA feature in RCL.
For representing PSOA RuleML expressions, syntactically similar to atoms, RCL omits `with` and changes the keyword `a` to `the` (prefixing the function).

## Contents

## 1 Introduction

The development of rule-based systems by end users (e.g., domain experts), especially when not in IT, can benefit from displaying rules not (only) in logical syntaxes but (also) in two intuition-targeting alternative syntaxes facilitating visualization and verbalization (ideally, jointly in both kinds of "v'alization"). For RuleML's logical syntaxes, particularly for PSOA RuleML's Presentation Syntax (PS), visualization is supported by Graph inscribed logic (Grailog), as explored in Data Systematics, and verbalization is supported by RuleML Controlled Language (RCL), as explored in the following (for examples of joint "v'alization" see A Hands-on PSOA RuleML Tutorial).

English-like paraphrasing of logical assertions (facts and rules) as well as queries provides a different angle for understanding them. Template equations (e.g., as in #RCL-PS_Mapping) for mapping between the English-like keyword syntax (e.g., RCL) and logical syntax (e.g., PS) can be employed in both directions:

- Mapping from logical to keyword syntax (e.g., PS to RCL) can assist domain experts in validating existing assertions and queries
- Mapping from keyword to logical syntax (e.g., RCL to PS) can assist domain experts in providing new assertions and posing new queries

For Artificial Intelligence (AI) based on logic or reconstructed with logic, direction 1. can also contribute to eXplainable AI (XAI) by verbalizing, respectively, logical Knowledge Bases (KBs) or logical-KB reconstructions of (deep) neural networks. The current document focuses on direction 2., which helps in understanding RuleML by syntactically progressing from the English-like RCL to the logical PS while preserving the semantics.

RCL is proposed generally for RuleML but expanded here initially for PSOA RuleML. At the center of (PSOA) RCL is another view of PSOA's systematics of positional-slotted object-applicative (psoa) atoms as elementary logical formulas, which can be employed in both assertions (e.g., data/ground facts) and queries as well as in (conclusions and conditions of) rules.

For psoa atoms in RCL, the keyword `thru` (highest precedence) aggregates terms to a tuple, `plus` (medium precedence) aggregates descriptors to either a predicate-dependent (`of`) or predicate-independent (`with`) sequence, and `alongside` (lowest precedence) aggregates `of`/`with`-prefixed descriptor sequences on an atom's top-level.

Because of the ubiquity of attribute-value pairs, e.g. in key-value stores and machine learning, and because direct juxtaposition nicely works in English, RCL does not rely on an (infixed) keyword for pairing what in PSOA RuleML is called a slot name with its filler. Instead, RCL uses name-filler juxtaposition as in `signal green` for PSOA's slot `signal->green`.

To represent a tuple of 2 or 3, etc. terms, RCL uses the (infixed) keyword `thru` as in `yellow thru green` or `red, yellow, thru green`, etc. for PSOA's (implicit) tuple `yellow green` or `red yellow green`, etc. For a tuple of 1 term, RCL omits `thru` as in `green`, while for the empty tuple it uses the keyword `emptup`.

To represent a sequence of 2 etc. descriptors (tuples, slots, or combined), RCL uses the (infixed) keyword `plus` as in `red, yellow, thru green plus signal green` (combining a single tuple and a single slot), equivalently `signal green plus red, yellow, thru green` (commutatively combining the same descriptors), etc. For a sequence of 1 descriptor, RCL omits `plus` as in the single-descriptor (single-tuple) examples of the previous paragraph and the single-descriptor (single-slot) example of the next-to-previous paragraph. Likewise, there is no room for `plus` in the empty descriptor sequence.

Each (descriptor) sequence is prefixed in RCL either by the keyword `of` to make it predicate-dependent or by the keyword `with` to make it predicate-independent.
The user can choose to put all of an atom's descriptors into one sequence, as in the predicate-dependent `of red, yellow, thru green plus signal green` (which is a shortcut for the `of`-'homogeneous' `of red, yellow, thru green alongside of signal green`, equivalently `of signal green alongside of red, yellow, thru green`); or, as in the predicate-independent `with red, yellow, thru green plus signal green` (which is a shortcut for the `with`-'homogeneous' `with red, yellow, thru green alongside with signal green`, equivalently `with signal green alongside with red, yellow, thru green`).
Alternatively, they can choose to distribute an atom's descriptors over multiple sequences, down to single-descriptor sequences, e.g. over the predicate-dependent `of red, yellow, thru green` and the predicate-independent `with signal green`, leading to `of red, yellow, thru green alongside with signal green`, equivalently `with signal green alongside of red, yellow, thru green` (as needed for the `of`/`with`-'heterogeneous' descriptor sequences in an (oidless) independent+dependent RCL atom like `lights of red, yellow, thru green alongside with signal green`, equivalently `lights with signal green alongside of red, yellow, thru green`).

The RCL keyword `alongside` is always followed by either the keyword `of` or `with`. Hence, the resulting key phrases `alongside of` and `alongside with` can be regarded as prefixes for predicate-dependent and -independent descriptor sequences. Summarizing, `alongside` is needed only for aggregating the 'heterogeneous' `with` and `of` sequences in independent+dependent atoms.
It can be optionally used (replacing `plus`) also for expanding the 'homogeneous' `with` or `of` sequences in independent or dependent atoms, respectively.

## 2 RCL Atoms

### 2.1 Relationships

The (oidful) RCL atom

a purchase of John, Mary, thru Fido

represents a `purchase` predicate establishing a 3-ary **relationship** between `John`, `Mary`, and `Fido`. The predicate is indicated by the RCL keyword `a`, and the (predicate-)dependent argument tuple by the keyword `of`), where the order within the (optionally, comma-punctuated) tuple is significant (indicated by the RCL keyword `thru`).

This can be mapped to an atom in PS by using a `purchase` predicate applied to three arguments, `John`, `Mary`, and `Fido`

purchase(John Mary Fido)

Since the order of the arguments is significant, these relationships are not equivalent to, respectively, `a purchase of Mary, John, thru Fido` and `purchase(Mary John Fido)`. Intuitively speaking, the different 'implicit roles' in a relationship, here including the buyer and the seller, need to be kept track of, which becomes non-trivial when there are many arguments.

### 2.2 Pairships, Framepoints, and Shelfpoints

For this reason, the `purchase` predicate can be alternatively represented as the following RCL atom. Three predicate-dependent slots are introduced by the keyword `of`, where each slot name, e.g. `buyer`, is directly paired with its filler, e.g. `John` (obtaining, e.g., `buyer` `John`), and the final pair is preceded by the keyword `plus`:

a purchase of buyer John, seller Mary, plus item Fido

This **pairship** can be mapped to the following PS
atom, using slot names ('explicit roles') `buyer`, `seller`, and `item`; the dependent-arrow infix, "`+>`", pairs a (predicate-)dependent slot name with its filler:

purchase(buyer+>John seller+>Mary item+>Fido)

Here, the three "`+`"-shafted *name*`+>`*filler* arrow constructs make explicit that there are multiple predicate-dependent ("`+`") slots.

While each slot is an (ordered) *name*/*filler* pair, the order between slots is immaterial, hence the above RCL and PS pairships are equivalent to all of their slot-permuted ones, including:

a purchase of seller Mary, buyer John, plus item Fido

purchase(seller+>Mary buyer+>John item+>Fido)

Changing the slots to predicate-independent and adding an Object IDentifier (OID), `transaction200`,
we obtain the following RCL **framepoint** atom. The OID is given before the predicate, the (predicate-)independent slots are indicated by the keyword `with`:

transaction200, a purchase with buyer John, seller Mary, plus item Fido

In PS, the representation becomes the following framepoint atom. The hash infix, "`#`", types an OID, here `transaction200`, with its predicate, i.e. indicates membership; the independent-arrow infix, "`->`", pairs an independent slot name with its filler:

transaction200#purchase(buyer->John seller->Mary item->Fido)

Rather than making the ordered `purchase` relationship slotted (obtaining a pairship) and then changing the slots to independent and adding an OID (obtaining a framepoint),
the relationship can be kept ordered, its tuple changed to (predicate-)independent and an OID be added, arriving at a **shelfpoint** atom. In PS, the (predicate-)independent tuple is indicated by a minus-signed explicit pair of square brackets:

transaction200, a purchase with John, Mary, thru Fido

transaction200#purchase(-[John Mary Fido])

### 2.3 Independent+Dependent Atoms

Besides the above four kinds of (relationship, pairship, framepoint, and shelfpoint) atoms,
RCL allows other kinds (for example, by systematic variation of the keywords `of` for (predicate-)dependent descriptors, e.g. dependent tuples, and `with` for (predicate-)independent descriptors, e.g. independent slots).
They reflect the corresponding PS systematics illustrated with the same examples at PSOA RuleML#Presentation_Preview.

In particular, the PSOA RuleML metamodel in Ref. 15, Appendix A, Fig. 5, allows for oidful tupled+slotted independent+dependent atoms (id6).
Since these have both dependent and independent descriptors, they use
both the keyword `of` and the keyword `with`, in descriptor sequences separated by the keyword `alongside`.

A simple id6 example blending the above relationship and framepoint examples, using one (predicate-)dependent sequence (specialized to a single tuple (containing two terms) and one (predicate-)independent descriptor sequence (specialized to a single slot), is the following:

In RCL:

transaction300, a purchase of John thru Mary alongside with item Fido

In PS:

transaction300#purchase(John Mary item->Fido)

A complementary id6 example, using one dependent sequence (specialized to a single tuple (containing one term) and one independent descriptor sequence (specialized to two slots), is the following:

In RCL:

transaction300, a purchase of John alongside with seller Mary plus item Fido

In PS:

transaction300#purchase(John seller->Mary item->Fido)

### 2.4 Atoms with Multiple Dependent Sequences

Moreover, RCL allows multiple dependent sequences.

In RCL (the second version showing an equivalent `alongside` expansion):

transaction300, a purchase of John thru Mary plus item Fido

transaction300, a purchase of John thru Mary alongside of item Fido

In PS (using implicit tuple):

transaction300#purchase(John Mary item+>Fido)

In PS (using explicit tuple):

transaction300#purchase(+[John Mary] item+>Fido)

Also for the complementary example, which now has three (rather than two) dependent descriptors:

In RCL (the second version showing an equivalent `alongside` expansion):

transaction300, a purchase of John, seller Mary, plus item Fido

transaction300, a purchase of John, of seller Mary, alongside of item Fido

In PS (using implicit tuple):

transaction300#purchase(John seller+>Mary item+>Fido)

In PS (using explicit tuple):

transaction300#purchase(+[John] seller+>Mary item+>Fido)

### 2.5 Atoms with Multiple Independent Sequences

Similarly, RCL allows multiple independent sequences.

In RCL (the second version showing an equivalent `alongside` expansion):

transaction300, a purchase with John thru Mary plus item Fido

transaction300, a purchase with John thru Mary alongside with item Fido

In PS (using explicit tuple):

transaction300#purchase(-[John Mary] item->Fido)

Also for the complementary example, which now has three (rather than two) independent descriptors:

In RCL (the second version showing an equivalent `alongside` expansion):

transaction300, a purchase with John, seller Mary, plus item Fido

transaction300, a purchase with John, with seller Mary, alongside with item Fido

In PS (using explicit tuple):

transaction300#purchase(-[John] seller->Mary item->Fido)

### 2.6 Atoms with Multiple Tuples

As penultimate alterations in this example series, RCL allows multiple tuples, where the order between tuples is immaterial, making the below atoms equivalent to their tuple-permuted ones.

RCL allows dependent multiple-tuple (e.g., two-tuple) sequences:

In RCL (in both permutations):

transaction300, a purchase of John thru Mary plus Fido

transaction300, a purchase of Fido plus John thru Mary

In PS (using explicit tuples, in both permutations):

transaction300#purchase(+[John Mary] +[Fido])

transaction300#purchase(+[Fido] +[John Mary])

RCL allows independent multiple-tuple (e.g., two-tuple) sequences:

In RCL (in both permutations):

transaction300, a purchase with John thru Mary plus Fido

transaction300, a purchase with Fido plus John thru Mary

In PS (using explicit tuples, in both permutations):

transaction300#purchase(-[John Mary] -[Fido])

transaction300#purchase(-[Fido] -[John Mary])

### 2.7 Atoms with Slots and Tuples

Finally, the `John thru Mary` tuple can again be replaced by slots named `buyer` and `seller`, while the `Fido` singleton tuple may be kept since `item` is not a very informative slot name.

RCL allows dependent two-slot-plus-singleton-tuple sequences:

In RCL (in three of six permutations):

transaction300, a purchase of buyer John, seller Mary, plus Fido

transaction300, a purchase of buyer John, Fido, plus seller Mary

transaction300, a purchase of Fido, buyer John, plus seller Mary

In PS (using explicit tuple, in three of six permutations):

transaction300#purchase(buyer+>John seller+>Mary +[Fido])

transaction300#purchase(buyer+>John +[Fido] seller+>Mary)

transaction300#purchase(+[Fido] buyer+>John seller+>Mary)

RCL allows independent two-slot-plus-singleton-tuple sequences:

In RCL (in three of six permutations):

transaction300, a purchase with buyer John, seller Mary, plus Fido

transaction300, a purchase with buyer John, Fido, plus seller Mary

transaction300, a purchase with Fido, buyer John, plus seller Mary

In PS (using explicit tuple, in three of six permutations):

transaction300#purchase(buyer->John seller->Mary -[Fido])

transaction300#purchase(buyer->John -[Fido] seller->Mary)

transaction300#purchase(-[Fido] buyer->John seller->Mary)

## 3 RCL Expressions

While the atoms so far have been on the function-free level of Datalog, constants like `Mary` as arguments can be refined to functional expressions of -- possibly nested -- (constructor-)function applications.

An expression is syntactically similar to an atom but has no OID and has only (function-)dependent descriptors.

In RCL, recall that the keyword `a` prefixes the operator of a term to distinguish it as the predicate of an atom. Complementarily, the keyword `the` prefixes the operator of a term to distinguish it as the function of an expression.

The following expression has an (implicit, dependent) tuple whose first element is an embedded expression having a length-1 tuple and whose second element is an embedded expression having another length-2 tuple:

In RCL (the top-level function symbol and the two embedded ones are indicated by the keyword `the`):

the store of the asset of Mary thru the place of TimesSquare thru NYC

In PS (the top-level function symbol is indicated by the caret prefix, "`^`", while the two embedded ones infer "`^`"):

^store(asset(Mary) place(TimesSquare NYC))

Substituting this expression for just `Mary` leads to the function-employing level of Horn logic, e.g. for the earlier relationship atom (#Relationships):

In RCL (the three embedded function symbols are indicated by the keyword `the`):

a purchase of John, the store of the asset of Mary thru the place of TimesSquare thru NYC, thru Fido

In PS (the three embedded function symbols infer "`^`"):

purchase(John store(asset(Mary) place(TimesSquare NYC)) Fido)

The following expression has two corresponding (dependent) slots where the `possession` slot uses the previous embedded length-1 expression and the `location` slot uses the embedded length-2 expression:

In RCL:

the store of possession the asset of Mary plus location the place of TimesSquare thru NYC

In PS:

^store(possession+>asset(Mary) location+>place(TimesSquare NYC))

Substituting this expression for `Mary` leads to the following, e.g. again for the earlier relationship atom (#Relationships):

In RCL:

a purchase of John, the store of possession the asset of Mary plus location the place of TimesSquare thru NYC, thru Fido

In PS:

purchase(John store(possession+>asset(Mary) location+>place(TimesSquare NYC)) Fido)

## 4 RCL Performatives and Rules

### 4.1 Asserting and Querying Atoms

To represent the RuleML `Assert` and `Query` performatives, RCL employs their names directly as keywords.

For assertions, RCL phrases (e.g., relationship and framepoint atoms), are preceded by the keyword `Assert`, and use a full stop at the end:

Relationship assertion (fact): Assert a purchase of John, Mary, thru Fido.

Framepoint assertion (fact): Assert transaction200, a purchase with buyer John, seller Mary, plus item Fido.

For queries, RCL phrases are preceded by the keyword `Query`, and use a question mark at the end, e.g.:

Relationship query: Query a purchase of John, Mary, thru Fido?

Framepoint query: Query transaction200, a purchase with buyer John, seller Mary, plus item Fido?

### 4.2 Non-Ground Atoms, Conjunctions/Disjunctions, and Rules

Atoms of RCL, like for PS, can also be non-ground, i.e. contain variables and expressions.

All of these RCL atoms can occur in a polyadic conjunction, infixed by `and`s, and in a polyadic disjunction, infixed by `or`s, which map, respectively, to the `And` and `Or` prefixes of PS.
All of the resulting RCL formulas can occur in a rule conclusion and condition separated by an `if` infix, which maps to the "`:-`" infix of PS.

## 5 RCL-PS Mapping of Atoms and Expressions

Equations are used to define a general bidirectional RCL-PS mapping for psoa terms (atoms and expressions), where an RCL term template on the left hand side (lhs) of an equation is paired with a PS term template on its right hand side (rhs).

In the following equations, each * bold-italic* symbol of the lhs-RCL (resp., rhs-PS) template is a metavariable co-referencing a

*metavariable of the paired rhs-PS (resp., lhs-RCL) template while being understood as the result of a recursive mapping application to its co-referenced lhs-RCL (resp., rhs-PS) metavariable.*

**bold-italic**Regarding the subscripts of the metavariables, the restrictions of Ref. 15, Section 4.1, apply, with the following additions (irrespective of the * +*/

*superscripts):*

**-**- Special tuples
- For a singleton tuple, i.e. if its
, with any subscripts, equals 1, the keyword**n**`thru`is omitted - For the empty tuple, i.e. if its
, with any subscripts, equals 0, the keyword**n**`thru`is also omitted and the keyword`emptup`is introduced

- For a singleton tuple, i.e. if its
- Special descriptor sequences
- For a singleton sequence, i.e. if its
,**m**, or**k**+**m**, with any subscripts, equals 1, the keyword**k**`plus`is omitted - For the empty sequence (of an empty atom), i.e. if its
,**m**, or**k**+**m**, with any subscripts, equals 0, the keyword**k**`plus`is also omitted

- For a singleton sequence, i.e. if its
- Special atoms
- For an atom that is not independent+dependent, i.e. if its
+**m**^{-}or**k**^{-}+**m**^{+}, with any subscripts, equals 0, the keyword**k**^{+}`alongside`is omitted

- For an atom that is not independent+dependent, i.e. if its

While the 2-dimensional "pretty-print"-indented layout using whitespace is not part of the -- machine-readable -- syntax in either RCL or PS, it does support their interpretation as -- human-readable -- languages (as exemplified in #RCL Expressions). The comma punctuation in RCL is optional (there is none in PS), since it does not carry information, but can further increase readabililty.

Regarding atoms, an OID, * o*, may occur in both the RCL and PS templates of an equation (in RCL followed by an optional comma, ", ") or in none, as indicated by the Cyan color.
Even if the

*is omitted in both, a "#" in PS may occur for top-level terms that are atoms and must occur for atoms embedded within other terms (where, contextually, expressions would be expected), as indicated by the Blue color.*

**o**Regarding expressions, a "^" in PS must occur for top-level terms that are expressions (where, contextually, atoms would be expected) and may occur for expressions embedded within other terms, as indicated by the Orange color.

The equations are systematically labeled by subscripted acronyms characterizing their lhs RCL, much of which also applies to their rhs PS. The first four equations map atoms (subscript A); the remaining two map expressions (subscript E). The acronyms start with an indication for contracted (lower-case letter c) vs. expanded (no lower-case letter) RCL forms / RCL normal forms. The upper-case acronym letters indicate left-dependent (LD) and left-tuple (LT) -- in either order -- forms (F) as well as normal forms (NF).

For equation (cLDLTF_{A}), the lhs template is a psoa atom in * of/with-contracted left-dependent, left-tuple form* (with dependent-before-independent ordering primary and tuple-before-slot secondary) of RCL, showing that one

`of`and one

`with`keyword per atom is sufficient. The rhs template is a corresponding atom in left-dependent, left-tuple form of PS.

* o*, a

*of*

**f***, ...,*

**t**^{+}_{1,1}*, thru*

**t**^{+}_{1,(n+1-1)}*,*

**t**^{+}_{1,n+1}. . .,

*, ...,*

**t**^{+}_{(m+-1),1}*, thru*

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*,*

**t**^{+}_{(m+-1),n+(m+-1)}*, ...,*

**t**^{+}_{m+,1}*, thru*

**t**^{+}_{m+,(n+m+-1)}*,*

**t**^{+}_{m+,n+m+}

**p**^{+}_{1}*, . . .,*

**v**^{+}_{1}

**p**^{+}_{(k+-1)}*, plus*

**v**^{+}_{(k+-1)}

**p**^{+}_{k+}*,*

**v**^{+}_{k+}alongside

with

*, ...,*

**t**^{-}_{1,1}*, thru*

**t**^{-}_{1,(n-1-1)}*,*

**t**^{-}_{1,n-1}. . .,

*, ...,*

**t**^{-}_{(m--1),1}*, thru*

**t**^{-}_{(m--1),(n-(m--1)-1)}*,*

**t**^{-}_{(m--1),n-(m--1)}*...*

**t**^{-}_{m-,1}*, thru*

**t**^{-}_{m-,(n-m--1)}*,*

**t**^{-}_{m-,n-m-}

**p**^{-}_{1}*, . . .,*

**v**^{-}_{1}

**p**^{-}_{(k--1)}*, plus*

**v**^{-}_{(k--1)}

**p**^{-}_{k-}

**v**^{-}_{k-}= (cLDLTF_{A})

* o*#

*(+[*

**f***...*

**t**^{+}_{1,1}

**t**^{+}_{1,(n+1-1)}*]*

**t**^{+}_{1,n+1}. . .

+[

*...*

**t**^{+}_{(m+-1),1}

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*]*

**t**^{+}_{(m+-1),n+(m+-1)}+[

*...*

**t**^{+}_{m+,1}

**t**^{+}_{m+,(n+m+-1)}*]*

**t**^{+}_{m+,n+m+}*+>*

**p**^{+}_{1}*. . .*

**v**^{+}_{1}*+>*

**p**^{+}_{(k+-1)}

**v**^{+}_{(k+-1)}*+>*

**p**^{+}_{k+}

**v**^{+}_{k+}-[

*...*

**t**^{-}_{1,1}

**t**^{-}_{1,(n-1-1)}*]*

**t**^{-}_{1,n-1}. . .

-[

*...*

**t**^{-}_{(m--1),1}

**t**^{-}_{(m--1),(n-(m--1)-1)}*]*

**t**^{-}_{(m--1),n-(m--1)}-[

*...*

**t**^{-}_{m-,1}

**t**^{-}_{m-,(n-m--1)}*]*

**t**^{-}_{m-,n-m-}*->*

**p**^{-}_{1}*. . .*

**v**^{-}_{1}*->*

**p**^{-}_{(k--1)}

**v**^{-}_{(k--1)}*->*

**p**^{-}_{k-}*)*

**v**^{-}_{k-}

For equation (LDLTF_{A}), the lhs template is the equivalent psoa atom in * of/with-expanded left-dependent, left-tuple form* of RCL, using PS-style single-descriptor sequences that in RCL require an

`of`and

`with`keyword for each dependent and independent descriptor, respectively. Hence the rhs template is a directly corresponding atom in left-dependent, left-tuple form of PS (the same as in equation (cLDLTF

_{A}) above), where

`of`... maps to a dependent descriptor +[...] or ...+>..., while

`with`... maps to an independent descriptor -[...] or ...->...

* o*, a

*of*

**f***, ...,*

**t**^{+}_{1,1}*, thru*

**t**^{+}_{1,(n+1-1)}*,*

**t**^{+}_{1,n+1}. . .,

of

*, ...,*

**t**^{+}_{(m+-1),1}*, thru*

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*,*

**t**^{+}_{(m+-1),n+(m+-1)}of

*, ...,*

**t**^{+}_{m+,1}*, thru*

**t**^{+}_{m+,(n+m+-1)}*,*

**t**^{+}_{m+,n+m+}of

**p**^{+}_{1}*, . . ., of*

**v**^{+}_{1}

**p**^{+}_{(k+-1)}*, of*

**v**^{+}_{(k+-1)}

**p**^{+}_{k+}*,*

**v**^{+}_{k+}with

*, ...,*

**t**^{-}_{1,1}*, thru*

**t**^{-}_{1,(n-1-1)}*,*

**t**^{-}_{1,n-1}. . .,

with

*, ...,*

**t**^{-}_{(m--1),1}*, thru*

**t**^{-}_{(m--1),(n-(m--1)-1)}*,*

**t**^{-}_{(m--1),n-(m--1)}with

*...*

**t**^{-}_{m-,1}*, thru*

**t**^{-}_{m-,(n-m--1)}*,*

**t**^{-}_{m-,n-m-}with

**p**^{-}_{1}*, . . ., with*

**v**^{-}_{1}

**p**^{-}_{(k--1)}*, alongside with*

**v**^{-}_{(k--1)}

**p**^{-}_{k-}

**v**^{-}_{k-}= (LDLTF_{A})

* o*#

*(+[*

**f***...*

**t**^{+}_{1,1}

**t**^{+}_{1,(n+1-1)}*]*

**t**^{+}_{1,n+1}. . .

+[

*...*

**t**^{+}_{(m+-1),1}

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*]*

**t**^{+}_{(m+-1),n+(m+-1)}+[

*...*

**t**^{+}_{m+,1}

**t**^{+}_{m+,(n+m+-1)}*]*

**t**^{+}_{m+,n+m+}*+>*

**p**^{+}_{1}*. . .*

**v**^{+}_{1}*+>*

**p**^{+}_{(k+-1)}

**v**^{+}_{(k+-1)}*+>*

**p**^{+}_{k+}

**v**^{+}_{k+}-[

*...*

**t**^{-}_{1,1}

**t**^{-}_{1,(n-1-1)}*]*

**t**^{-}_{1,n-1}. . .

-[

*...*

**t**^{-}_{(m--1),1}

**t**^{-}_{(m--1),(n-(m--1)-1)}*]*

**t**^{-}_{(m--1),n-(m--1)}-[

*...*

**t**^{-}_{m-,1}

**t**^{-}_{m-,(n-m--1)}*]*

**t**^{-}_{m-,n-m-}*->*

**p**^{-}_{1}*. . .*

**v**^{-}_{1}*->*

**p**^{-}_{(k--1)}

**v**^{-}_{(k--1)}*->*

**p**^{-}_{k-}*)*

**v**^{-}_{k-}

For equation (cLTLDNF_{A}), the lhs template is the equivalent psoa atom in * of/with-contracted left-tuple, left-dependent normal form* (with tuple-before-slot ordering primary and dependent-before-independent secondary) of RCL, requiring two

`of`and two

`with`keywords. The rhs template is the corresponding atom in left-tuple, left-dependent normal form of PS.

* o*, a

*of*

**f***, ...,*

**t**^{+}_{1,1}*, thru*

**t**^{+}_{1,(n+1-1)}*,*

**t**^{+}_{1,n+1}. . .,

*, ...,*

**t**^{+}_{(m+-1),1}*, thru*

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*,*

**t**^{+}_{(m+-1),n+(m+-1)}plus

*, ...,*

**t**^{+}_{m+,1}*, thru*

**t**^{+}_{m+,(n+m+-1)}*,*

**t**^{+}_{m+,n+m+}with

*, ...,*

**t**^{-}_{1,1}*, thru*

**t**^{-}_{1,(n-1-1)}*,*

**t**^{-}_{1,n-1}. . .,

*, ...,*

**t**^{-}_{(m--1),1}*, thru*

**t**^{-}_{(m--1),(n-(m--1)-1)}*,*

**t**^{-}_{(m--1),n-(m--1)}plus

*...*

**t**^{-}_{m-,1}*, thru*

**t**^{-}_{m-,(n-m--1)}*,*

**t**^{-}_{m-,n-m-}of

**p**^{+}_{1}*, . . .,*

**v**^{+}_{1}

**p**^{+}_{(k+-1)}*, plus*

**v**^{+}_{(k+-1)}

**p**^{+}_{k+}*,*

**v**^{+}_{k+}alongside

with

**p**^{-}_{1}*, . . .,*

**v**^{-}_{1}

**p**^{-}_{(k--1)}*, plus*

**v**^{-}_{(k--1)}

**p**^{-}_{k-}

**v**^{-}_{k-}= (cLTLDNF_{A})

* o*#

*(+[*

**f***...*

**t**^{+}_{1,1}

**t**^{+}_{1,(n+1-1)}*]*

**t**^{+}_{1,n+1}. . .

+[

*...*

**t**^{+}_{(m+-1),1}

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*]*

**t**^{+}_{(m+-1),n+(m+-1)}+[

*...*

**t**^{+}_{m+,1}

**t**^{+}_{m+,(n+m+-1)}*]*

**t**^{+}_{m+,n+m+}-[

*...*

**t**^{-}_{1,1}

**t**^{-}_{1,(n-1-1)}*]*

**t**^{-}_{1,n-1}. . .

-[

*...*

**t**^{-}_{(m--1),1}

**t**^{-}_{(m--1),(n-(m--1)-1)}*]*

**t**^{-}_{(m--1),n-(m--1)}-[

*...*

**t**^{-}_{m-,1}

**t**^{-}_{m-,(n-m--1)}*]*

**t**^{-}_{m-,n-m-}*+>*

**p**^{+}_{1}*. . .*

**v**^{+}_{1}*+>*

**p**^{+}_{(k+-1)}

**v**^{+}_{(k+-1)}*+>*

**p**^{+}_{k+}

**v**^{+}_{k+}*->*

**p**^{-}_{1}*. . .*

**v**^{-}_{1}*->*

**p**^{-}_{(k--1)}

**v**^{-}_{(k--1)}*->*

**p**^{-}_{k-}*)*

**v**^{-}_{k-}

For equation (LTLDNF_{A}), the lhs template is the equivalent psoa atom in * of/with-expanded left-tuple, left-dependent normal form* of RCL, using PS-style single-descriptor sequences that in RCL require an

`of`and

`with`keyword for each dependent and independent descriptor, respectively. Hence the rhs template is a directly corresponding atom in left-tuple, left-dependent normal form of PS (the same as in equation (cLTLDNF

_{A}) above).

* o*, a

*of*

**f***, ...,*

**t**^{+}_{1,1}*, thru*

**t**^{+}_{1,(n+1-1)}*,*

**t**^{+}_{1,n+1}. . .,

of

*, ...,*

**t**^{+}_{(m+-1),1}*, thru*

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*,*

**t**^{+}_{(m+-1),n+(m+-1)}of

*, ...,*

**t**^{+}_{m+,1}*, thru*

**t**^{+}_{m+,(n+m+-1)}*,*

**t**^{+}_{m+,n+m+}with

*, ...,*

**t**^{-}_{1,1}*, thru*

**t**^{-}_{1,(n-1-1)}*,*

**t**^{-}_{1,n-1}. . .,

with

*, ...,*

**t**^{-}_{(m--1),1}*, thru*

**t**^{-}_{(m--1),(n-(m--1)-1)}*,*

**t**^{-}_{(m--1),n-(m--1)}with

*...*

**t**^{-}_{m-,1}*, thru*

**t**^{-}_{m-,(n-m--1)}*,*

**t**^{-}_{m-,n-m-}of

**p**^{+}_{1}*, . . ., of*

**v**^{+}_{1}

**p**^{+}_{(k+-1)}*, of*

**v**^{+}_{(k+-1)}

**p**^{+}_{k+}*,*

**v**^{+}_{k+}with

**p**^{-}_{1}*, . . ., with*

**v**^{-}_{1}

**p**^{-}_{(k--1)}*, alongside with*

**v**^{-}_{(k--1)}

**p**^{-}_{k-}

**v**^{-}_{k-}= (LTLDNF_{A})

* o*#

*(+[*

**f***...*

**t**^{+}_{1,1}

**t**^{+}_{1,(n+1-1)}*]*

**t**^{+}_{1,n+1}. . .

+[

*...*

**t**^{+}_{(m+-1),1}

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*]*

**t**^{+}_{(m+-1),n+(m+-1)}+[

*...*

**t**^{+}_{m+,1}

**t**^{+}_{m+,(n+m+-1)}*]*

**t**^{+}_{m+,n+m+}-[

*...*

**t**^{-}_{1,1}

**t**^{-}_{1,(n-1-1)}*]*

**t**^{-}_{1,n-1}. . .

-[

*...*

**t**^{-}_{(m--1),1}

**t**^{-}_{(m--1),(n-(m--1)-1)}*]*

**t**^{-}_{(m--1),n-(m--1)}-[

*...*

**t**^{-}_{m-,1}

**t**^{-}_{m-,(n-m--1)}*]*

**t**^{-}_{m-,n-m-}*+>*

**p**^{+}_{1}*. . .*

**v**^{+}_{1}*+>*

**p**^{+}_{(k+-1)}

**v**^{+}_{(k+-1)}*+>*

**p**^{+}_{k+}

**v**^{+}_{k+}*->*

**p**^{-}_{1}*. . .*

**v**^{-}_{1}*->*

**p**^{-}_{(k--1)}

**v**^{-}_{(k--1)}*->*

**p**^{-}_{k-}*)*

**v**^{-}_{k-}

For equation (cLTNF_{E}), the lhs template is a psoa expression in * of-contracted left-tuple normal form* (all descriptors being dependent, with tuple-before-slot ordering only) of RCL, showing that one

`of`keyword per expression is sufficient. The rhs template is a corresponding expression in left-tuple normal form of PS.

the * f* of

*, ...,*

**t**^{+}_{1,1}*, thru*

**t**^{+}_{1,(n+1-1)}*,*

**t**^{+}_{1,n+1}. . .,

*, ...,*

**t**^{+}_{(m+-1),1}*, thru*

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*,*

**t**^{+}_{(m+-1),n+(m+-1)}*, ...,*

**t**^{+}_{m+,1}*, thru*

**t**^{+}_{m+,(n+m+-1)}*,*

**t**^{+}_{m+,n+m+}

**p**^{+}_{1}*, . . .,*

**v**^{+}_{1}

**p**^{+}_{(k+-1)}*, plus*

**v**^{+}_{(k+-1)}

**p**^{+}_{k+}

**v**^{+}_{k+}= (cLTNF_{E})

^* f*(+[

*...*

**t**^{+}_{1,1}

**t**^{+}_{1,(n+1-1)}*]*

**t**^{+}_{1,n+1}. . .

+[

*...*

**t**^{+}_{(m+-1),1}

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*]*

**t**^{+}_{(m+-1),n+(m+-1)}+[

*...*

**t**^{+}_{m+,1}

**t**^{+}_{m+,(n+m+-1)}*]*

**t**^{+}_{m+,n+m+}*+>*

**p**^{+}_{1}*. . .*

**v**^{+}_{1}*+>*

**p**^{+}_{(k+-1)}

**v**^{+}_{(k+-1)}*+>*

**p**^{+}_{k+}*)*

**v**^{+}_{k+}

For equation (LTNF_{E}), the lhs template is the equivalent psoa expression in * of-expanded left-tuple normal form* of RCL, using PS-style single-descriptor sequences that in RCL require an

`of`for each descriptor. Hence the rhs template is a directly corresponding expression in left-tuple normal form of PS (the same as in equation (cLTNF

_{E}) above), where

`of`... maps to a dependent descriptor +[...] or ...+>...

the * f* of

*, ...,*

**t**^{+}_{1,1}*, thru*

**t**^{+}_{1,(n+1-1)}*,*

**t**^{+}_{1,n+1}. . .,

of

*, ...,*

**t**^{+}_{(m+-1),1}*, thru*

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*,*

**t**^{+}_{(m+-1),n+(m+-1)}of

*, ...,*

**t**^{+}_{m+,1}*, thru*

**t**^{+}_{m+,(n+m+-1)}*,*

**t**^{+}_{m+,n+m+}of

**p**^{+}_{1}*, . . ., of*

**v**^{+}_{1}

**p**^{+}_{(k+-1)}*, of*

**v**^{+}_{(k+-1)}

**p**^{+}_{k+}

**v**^{+}_{k+}= (LTNF_{E})

^* f*(+[

*...*

**t**^{+}_{1,1}

**t**^{+}_{1,(n+1-1)}*]*

**t**^{+}_{1,n+1}. . .

+[

*...*

**t**^{+}_{(m+-1),1}

**t**^{+}_{(m+-1),(n+(m+-1)-1)}*]*

**t**^{+}_{(m+-1),n+(m+-1)}+[

*...*

**t**^{+}_{m+,1}

**t**^{+}_{m+,(n+m+-1)}*]*

**t**^{+}_{m+,n+m+}*+>*

**p**^{+}_{1}*. . .*

**v**^{+}_{1}*+>*

**p**^{+}_{(k+-1)}

**v**^{+}_{(k+-1)}*+>*

**p**^{+}_{k+}*)*

**v**^{+}_{k+}