This paper discusses extensions of RuleML and TPTP for higher-order logic, modal logic, and higher-order modal logic. For these extensions, an extended XSLT 2.0-based translator is presented which maps from RuleML/XML to TPTP. With this implemented HOML RuleM2TPTP tool, TPTP can benefit from RuleML interoperation and much of Deliberation RuleML can execute on TPTP-aware provers.
Like this earlier FOL RuleML2TPTP, the newly implemented HOML
RuleML2TPTP performs recursive case analysis to linearize XML trees to TPTP
texts. The generated TPTP syntax can be validated and executed with
TPTPaware higher-order ATP systems such as Leo-II [
The current paper is organized as follows. Section 2 presents the evolving HOML TPTP. Section 3 proposes the new HOML RuleML. Section 4 describes the RuleML-to-TPTP translation method. Section 5 illustrates the translation with examples. Section 6 explains the XSLT-based translator. Finally, Section 7 gives conclusions. 2
HOML extends higher-order classical logic with a (multi-)modal logic using a countable set of (parameterized) dual pairs of abstract modal ‘box’/‘diamond’ operators, where the first two pairs might be instantiated to, e.g., ‘necessary’/ ‘possible’ (alethically) and ‘obligatory’/‘permissible’ (deontically).
For higher-order classical logic the TPTP THF languages have been proposed
[
To capture typed higher-order modal logics, another extension of TH0, called
THM, is currently under development [
In TH0, which is a concrete syntax for HOL, $i and $o represent the HOL base types i (individuals) and o (Booleans). $i>$o encodes a function (predicate) type. Predicate application, as in A(X; W ), is encoded as in ((A@X)@W) or simply in (A@X@W), i.e. function/predicate application is represented by @; universal quantification and -abstraction, as in Ai!o8WiA(W ), are encoded as in ˆ[A:$i>$o]:![W:$i]:(A@W). 3
HOML RuleML is an advancement plus combination of Functional RuleML [
Since HOL RuleML considers predicates (relations) as characteristic
(booleanvalued) functions, it applies both of these via RuleML’s Uniterms,
generalizing Atoms and Expressions:10 Constants are employed as the operators of
Uniterms, generalizing Relations of Atoms and Functions of Expressions (as
well as Individuals).11 While formulas point to, e.g., Atoms, the RIF-FLD-like
termulas [
For the type level, HOL RuleML proposes a Tbase (“Type base”) element whose PCDATA currently correspond to $i and $o (without the “$” prefix). On top of this, two further RuleML/XML elements are proposed: Entitype associates an entity (e.g., a Variable) with a type (e.g., a Tbase or a Tmap); Tmap (“Type map”) combines – into a function type – a domain type and a codomain type, both of which may again be Tmap types etc., down to any level of nesting.
Since ML RuleML provides a countable set pairing ‘necessary’-like parameterized ‘box’ operators with dual ‘possible’-like parameterized ‘diamond’ operators, it is more abstract than Modal RuleML 1.0. Also, ML RuleML is more expressive since, instead of an Atom element with a modal-attributed Relation and a modally embedded atom, ML RuleML uses a new Modal element with a variety edge leading to Box or Diamond elements and a proposition edge leading to a modally embedded arbitrary formula. 4
To avoid extending FOL RuleML2TPTP’s preprocessing to HOML RuleML/XML using a (yet to be extended) RuleML normalizer, a fully striped normal form12 is assumed as the input for translation to TPTP output. This form gives XML trees an object-oriented flavor by alternating (upper-cased <Node>) object elements with (lower-cased <edge>) property subelements. Like for earlier subfamilies of Deliberation RuleML, the HOML RuleML normalizer will need to, e.g., reconstruct missing <edge> tags, making all omitted information explicit.
The translation from this normalized XML syntax to the TPTP syntax is specified by mapping tables defining recursive translation functions langbelow: Each row containing xml in the first column and tptp in the second column indicates a translation case lang(xml) = tptp, where – for most of the key language constructs (beyond FOL) considered here – tptp is composed from the results of recursive applications of lang(xmli) to parts xmli of xml. 9 http://ruleml.org/1.02/profiles/fodal. 10 http://wiki.ruleml.org/index.php/Glossary_of_Deliberation_RuleML_1.02# .3CUniterm.3E. 11 http://wiki.ruleml.org/index.php/Glossary_of_Deliberation_RuleML_1.02# .3CConst.3E. 12 http://wiki.ruleml.org/index.php/Specification_of_Deliberation_RuleML_ 1.02#XSLT-Based_Normalizer.
In Table 1, the mapping of the key higher-order language constructs with equality (which was already implemented in FOL RuleML2TPTP) and types is given as a translation function HO. (ˆ [ HO(t1), ... , HO(tn)] : HO(t)) HO(t1): HO(t2) ( HO(t1) > HO(t2)) $i $o
In Table 2, the mapping of the key modal language constructs is given as a translation function M .
The combination of the HO and M mappings results in the HOML mapping. 5
The following demo examples of RuleML-to-TPTP translation pairs are available from a GitHub test directory.13 13 https://github.com/RuleML/RuleML2TPTP/blob/homl/src/test/resources/ test/translator/HOMLRuleML2TPTP/.
The initial two examples take HOL TPTP from [
The first example shows the RuleML-TPTP translation pair for serializing union = X !o; Y !o; U ((X U ) _ (Y U )). <Equal> <left><Const>union</Const></left> <right> <Lambda> <declare> <Entitype> <entity>
<Var>X</Var> </entity> <type> <Tmap> <domain><Tbase>i</Tbase></domain> <codomain><Tbase>o</Tbase></codomain> </Tmap> </type> </Entitype> </declare> <declare> <Entitype> <entity>
<Var>Y</Var> </entity> <type> <Tmap> <domain><Tbase>i</Tbase></domain> <codomain><Tbase>o</Tbase></codomain> 14 Since the TPTP language identifier (thf or hmf) and name of a TPTP formula are currently not specified on the RuleML/XML level, they are not yet deployed in the implemented translator.
</Tmap> </type> </Entitype> </declare> <declare> <Entitype> <entity>
<Var>U</Var> </entity> <type>
<Tbase>i</Tbase> </type> </Entitype> </declare> <termula> <Or> <termula> <Uniterm> <op><Var>X</Var></op> <arg><Var>U</Var></arg> </Uniterm> </termula> <termula> <Uniterm> <op><Var>Y</Var></op> <arg><Var>U</Var></arg> </Uniterm> </termula> </Or> </termula> </Lambda> </right> </Equal> thf(union,definition, ( union = ( ^ [X:($i > $o),Y:($i > $o),U:$i] : ( ( X @ U ) | ( Y @ U ) ) ) )).
The second example shows the RuleML-TPTP translation pair serializing 8A !o8B !o8C !o((A [ (B \ C)) = ((A [ B) \ (A [ C))).
Here, binary (generally, n-ary) function applications are used instead of Currying into nested unary applications (although these are possible too), since both RuleML’s Uniterms and TPTP’s @ infixes admit n-ary applications. <Forall> <declare> <Entitype> <entity> <Var>A</Var> </entity> <type> <Tmap> <domain><Tbase>i</Tbase></domain> <codomain><Tbase>o</Tbase></codomain> </Tmap> </type> </Entitype> </declare> <declare> <Entitype> <entity>
<Var>B</Var> </entity> <type> <Tmap> <domain><Tbase>i</Tbase></domain> <codomain><Tbase>o</Tbase></codomain> </Tmap> </type> </Entitype> </declare> <declare> <Entitype> <entity>
<Var>C</Var> </entity> <type> <Tmap> <domain><Tbase>i</Tbase></domain> <codomain><Tbase>o</Tbase></codomain> </Tmap> </type> </Entitype> </declare> <termula> <Equal> <left> <Uniterm> <op><Const>union</Const></op> <arg><Var>A</Var></arg> <arg> <Uniterm> <op><Const>intersection</Const></op> <arg><Var>B</Var></arg> <arg><Var>C</Var></arg> </Uniterm> </arg> </Uniterm> </left> <right> <Uniterm> <op><Const>intersection</Const></op> <arg> <Uniterm> <op><Const>union</Const></op> <arg><Var>A</Var></arg> <arg><Var>B</Var></arg> </Uniterm> </arg> <arg> <Uniterm> <op><Const>union</Const></op> <arg><Var>A</Var></arg> <arg><Var>C</Var></arg> </Uniterm> </arg> </Uniterm> </right> </Equal> </termula> </Forall>
The third example of a RuleML-TPTP pair illustrates the normalized ML
RuleML/XML for a mapping-target ML TPTP formula that is specialized from
[
<Box><arg><Const>a</Const></arg></Box> </variety> <proposition> <Forall> <declare><Var>X</Var></declare> <formula> <Atom> <op><Rel>p</Rel></op> <arg><Var>X</Var></arg> </Atom> 15 We use fmf for didactic purposes, as a specialization of the hmf language identifier. </formula> </Forall> </proposition> </Modal> </if> <then> <Modal> <variety>
<Dia><arg><Const>b</Const></arg></Dia> </variety> <proposition> <Exists> <declare><Var>X</Var></declare> <formula> <Atom> <op><Rel>p</Rel></op> <arg><Var>X</Var></arg> </Atom> </formula> </Exists> </proposition> </Modal> </then> </Implies> fmf(1, conjecture, ( (#box(a): ( ! [X]: p(X) )) => (#dia(b): ( ? [X]: p(X) )) )).
The fourth RuleML-TPTP-pairing example, extending the third, illustrates
the syntax of normalized HOML RuleML/XML for the syntax of a HOML TPTP
formula as the mapping target taken unchanged from [
<arg><Var>X</Var></arg> </Uniterm> </termula> </Forall> </proposition> </Modal> </if> <then> <Modal> <variety>
<Dia><arg><Const>b</Const></arg></Dia> </variety> <proposition> <Exists> <declare> <Entitype> <entity><Var>X</Var></entity> <type><Tbase>i</Tbase></type> </Entitype> </declare> <termula> <Uniterm> <op><Rel>p</Rel></op> <arg><Var>X</Var></arg> </Uniterm> </termula> </Exists> </proposition> </Modal> </then> </Implies> hmf(2, conjecture, ( (#box(a): ( ! [X:$i]: ( p @ X ) )) => (#dia(b): ( ? [X:$i]: ( p @ X ) )) )).
Because of the universal and existential quantification over individuals and because of the different box/dia arguments a vs. b, the above example is a firstorder multi-modal logic conjecture. Since propositional and first-order (multi-) modal logics are fragments of higher-order (multi-)modal logic, any TPTP-aware prover or model finder for HOML will be applicable to it to analyze its validity (e.g., it is countersatisfiable in a multi-modal version of logic K, while it would be valid after replacing the dia argument b with a in modal logic S4). 6
Our translator from the new HOML RuleML to the emerging TPTP for HOML is realized as an extension of the earlier RuleML2TPTP translator from FOL RuleML to TPTP FOF. Furthermore, as is shown in the second column of Tables 1 and 2 in Section 4, the TPTP constructs are generated as a combination of the symbols of the emerging TPTP for HOML with the results of calling the earlier FOL translation function.
The new table-defined translation functions HO and M are implemented in XSLT 2.0. Each row of the tables leads to a corresponding XSLT template, which describes in detail the mapping from HOML RuleML to TPTP.
Note that the namespace prefix “ r:” for elements is defined at the beginning of the XSLT file, expanding to the RuleML namespace “http://ruleml.org/spec”.
The extended translator is available as a GitHub source file.16 6.1
Translating Higher-Order Constructs The HOL translator defines seven XSLT templates to map the XML elements specified for the translation function HO as the seven rows of Table 1.
For example, the template for the Entitype element is defined as follows: <xsl:template match="r:Entitype"> <xsl:apply-templates select="r:entity"/> <xsl:text>:</xsl:text> <xsl:apply-templates select="r:type"/> </xsl:template>
This XSLT definition maps the RuleML/XML Entitype prefix notation to a TPTP “:” infix notation. The apply-templates calls on both sides of the generated “:” text realize the HO recursions in Table 1. 6.2
Translating Modal Constructs The ML translator defines three XSLT templates to map the XML elements specified for the translation function M as the three rows of Table 2.
For example, the template for the Modal element is defined as follows: <xsl:template match="r:Modal"> <xsl:text>(</xsl:text> <xsl:apply-templates select="r:variety"/> <xsl:text>: (</xsl:text> <xsl:apply-templates select="r:proposition"/> <xsl:text>))</xsl:text> </xsl:template>
This XSLT definition maps the RuleML/XML Modal prefix notation to a TPTP “:” infix notation. The apply-templates calls on both sides of the generated “: (” text realize the M recursions in Table 2. 16 https://github.com/RuleML/RuleML2TPTP/blob/homl/src/main/resources/ xslt/ruleml2tptp.xslt.
This joint effort continues work that was done separately in the RuleML and TPTP communities: Extensions of both systems for (typed) higher-order logic, modal logic, and combined higher-order modal logic. RuleML’s new HOML RuleML/XML, mapping to the evolving HOML TPTP, already provided feedback17 to TPTP. The resulting XSLT-based translator, HOML RuleML2TPTP, characterizes the proposed HOL and HOML RuleML/XML extension and allows experimenting with HOL and HOML RuleML/XML examples executed by TPTPaware ATPs for HOL and HOML such as Leo-III.
Future work includes: Mapping RuleML performatives to TPTP roles;
defining HOML RuleML with the XML-schema language Relax NG; identifying the
language (e.g., as anchors18 corresponding to TPTP’s thf or hmf) in RuleML/
XML instances (e.g., via schemaLocation); adapting the current translator
for mapping this language identifier to TPTP along with reusing the FOL
RuleML2TPTP name generator for HOML RuleML2TPTP’s TPTP formulas;
implementing an inverse translator, HOML TPTP2RuleML; detailing the
correspondences between the earlier Functional RuleML and Modal RuleML and the
new HOL RuleML and ML RuleML; as well as introducing RuleML signature
declarations (e.g., starting with those in POSL [
We thank Gen Zou for his helpful suggestions, which led to improvements of the proposed HOML RuleML/XML and of this paper. Likewise, we thank the reviewers for their constructive comments as well as the chairs of the 10th International Rule Challenge for organizing this event. The first two authors are grateful to their host, Edward Zalta, at the Center for the Study of Language and Information, Stanford University, for providing an inspiring environment for starting this work. The first author thanks NSERC for its support through Discovery Grants. The work of the second author has been supported by the German Research Foundation DFG under reference number BE2501/9-2. 17 About parenthesizing TPTP type-mapping formulas, corresponding to RuleML Tmaps, and considering possible future replacement of some kinds of colon infixes with alternative infix characters. 18 http://deliberation.ruleml.org/1.02/relaxng/#anchor. 19 http://wiki.ruleml.org/index.php/Glossary_of_Reaction_RuleML_1.02# .3Csignature.3E. 20 http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml#THF%20formulae.