TPTP RuleML

From RuleML Wiki
Jump to: navigation, search

Authors: Meng Luan, Harold Boley


This version: TPTP RuleML

Latest version: TPTP RuleML

Previous versions:


1 Introduction

The "Thousands of Problems for Theorem Provers" Library (TPTP Library) is a comprehensive collection of Automated Theorem Proving (ATP) test problems, which are available, online, in a format often called the TPTP Syntax. The TPTP site (http://www.tptp.org) provides support for the testing and evaluation of ATP systems. It also hosts online services for invoking a large number of systems. The TPTP Syntax is enforced as the standard input format for all hosted ATP systems. In the following, "TPTP" will be used as a shorthand for "TPTP Syntax".

This TPTP RuleML page bridges between TPTP and RuleML. It serves as a documentation and planning page for the joint endeavors of the RuleML and TPTP communities.

2 Translations

There are two TPTP RuleML projects under development, one for each direction of the translation between subsets of RuleML/XML and TPTP, as expanded in the following subsections.

  • RuleML2TPTP: This project implements the XSLT 2.0-based translation from RuleML/XML to TPTP. See the project entry page for more information.
  • TPTP2RuleML: This project is still at the planning stage.

3 FOL RuleML2TPTP

The FOL RuleML2TPTP tool translates First-Order Logic (FOL) from RuleML to TPTP, as described and implemented at the above RuleML2TPTP link.

3.1 Use cases

3.1.1 WineOnto in TPTP

The RuleML use case WineOnto now has a TPTP version translated by the RuleML2TPTP tool from the Deliberation RuleML 1.01 version. Additional queries against WineOnto are as follows:

   ?- alsatianwine(?X).
   ?- americanwine(?X).
   ?- bordeaux(?X).
   ?- burgundy(?X).
   ?- anjou(?X).
   ?- beaujolais(?X).
   ?- cabernetfranc(?X).
   ?- cabernetsauvignon(?X).
   ?- californiawine(?X).
   ?- chardonnay(?X).
   ?- cheninblanc(?X).
   ?- chianti(?X).
   ?- cotesdor(?X).
   ?- dessertwine(?X).
   ?- dryriesling(?X).
   ?- dryredwine(?X).
   ?- drywhitewine(?X).
   ?- drywine(?X).
   ?- earlyharvest(?X).
   ?- frenchwine(?X).
   ?- fullbodiedwine(?X).
   ?- gamay(?X).
   ?- germanwine(?X).
   ?- grape(?X).
   ?- icewine(?X).
   ?- italianwine(?X).
   ?- lateharvest(?X).
   ?- loire(?X).
   ?- margaux(?X).
   ?- medoc(?X).
   ?- meritage(?X).
   ?- merlot(?X).
   ?- meursault(?X).
   ?- muscadet(?X).
   ?- pauillac(?X).
   ?- petitesyrah(?X).
   ?- pinotblanc(?X).
   ?- pinotnoir(?X).
   ?- port(?X).
   ?- potableliquid(?X).
   ?- redbordeaux(?X).
   ?- redburgundy(?X).
   ?- redtablewine(?X).
   ?- redwine(?X).
   ?- region(?X).
   ?- riesling(?X).
   ?- rosewine(?X).
   ?- sancerre(?X).
   ?- sauternes(?X).
   ?- sauvignonblanc(?X).
   ?- semillon(?X).
   ?- semillonorsauvignonblanc(?X).
   ?- stemilion(?X).
   ?- sweetriesling(?X).
   ?- sweetwine(?X).
   ?- tablewine(?X).
   ?- texaswine(?X).
   ?- tours(?X).
   ?- vintage(?X).
   ?- vintageyear(?X).
   ?- whitebordeaux(?X).
   ?- whiteburgundy(?X).
   ?- whiteloire(?X).
   ?- whitenonsweetwine(?X).
   ?- whitetablewine(?X).
   ?- whitewine(?X).
   ?- wine(?X).
   ?- winebody(?X).
   ?- winecolor(?X).
   ?- winedescriptor(?X).
   ?- wineflavor(?X).
   ?- winegrape(?X).
   ?- winesugar(?X).
   ?- winery(?X).
   ?- winetaste(?X).
   ?- zinfandel(?X).
   ?- adjacentregion(?X,?Y).
   ?- hasbody(?X,?Y).
   ?- hascolor(?X,?Y).
   ?- hasflavor(?X,?Y).
   ?- hasmaker(?X,?Y).
   ?- hassugar(?X,?Y).
   ?- hasvintageyear(?X,?Y).
   ?- haswinedescriptor(?X,?Y).
   ?- locatedin(?X,?Y).
   ?- madefromgrape(?X,?Y).
   ?- madefromfruit(?X,?Y).
   ?- madeintowine(?X,?Y).
   ?- produceswine(?X,?Y).

The above queries are shown in a straightforward presentation syntax: "?-" is the query prompt (as in Prolog) and "?" is the variable prefix (as in many other languages). Existential quantification is understood for any variables in queries. Note that not all of the above queries are satisfiable against the WineOnto knowledge base and facts. The RuleML version of the above queries was generated by a utility tool, and the TPTP version was generated by this RuleML2TPTP tool. Along with the WineOnto knowledge base and facts in TPTP, the conjunction of the satisfiable queries, as well as some harder ones of the unsatisfiable queries, may be adopted by the TPTP library in future.

3.1.2 Geospatial RBDA

As a preparatory task of a planned follow-up to Rule-Based Data Access, a Datalog-like program was implemented, containing the knowledge base, facts, and queries. It is given in the same presentation syntax as the one in the previous section. Universal quantification is understood for any variables in rules. The RuleML version of this program was also generated by the above-linked P2RuleML utility tool. Note that the resulting RuleML document transited to the Hornlog+ level because of the function applications in the original program. The TPTP version was then generated by this RuleML2TPTP tool. However, because the original document contains arithmetic built-ins, which are usually not provided by pure first-order logic provers, the TPTP version of this program cannot currently be executed by the ATP systems on the TPTP site.

4 HOML RuleML2TPTP

The HOML RuleML2TPTP tool translates Higher-Order Modal Logic (HOML) from RuleML to TPTP, as described in a paper and talk of the 10th International Rule Challenge at RuleML 2016 (CEUR Proceedings), and implemented at GitHub.

5 FOL TPTP2RuleML

5.1 Planning

The following is an investigation on the possibility of reusing some existing TPTP parsers.

5.1.1 Preferences

  • Java is preferred as the development language.
  • Apache Maven is preferred as the build tool.

5.1.2 Potential Problems

  • Comments may be ignored by the parser (or, shall we keep the comments?).
  • How to deal with 'include' in the TPTP files.
    • Expand
      • Cons: Complicated code. Add redundancy.
      • Pros: Integrated and independent output files.
    • Retain and Translate
      • Cons: RuleML/XML does not have this syntax/semantics.
      • Pros: Easy coding. Consistent with the original files.
    • Annotate (seems best)
      • Cons: Need applications to support.
      • Pros: Easy coding. RuleML/XML compatible.

5.1.3 TPTP Parsers

After correspondence between the RuleML and TPTP communities, a possible solution is to convert the TPTP syntax BNF to an ANTLR grammer and base the TPTP2RuleML translator on that.

5.1.3.1 JJ Parser in the TPTP Website's Service Tools
  • In C.
  • Parses a file into an internal structure.
  • Comprehensive/complex and no documentation for usage/APIs.
  • Not a dedicated parser. Includes APIs to convert TPTP to other formats and to manipulate the system on TPTP (guessed from the names of header files and functions).
  • Probably up-to-date (modified less than a year ago) and used by TPTP4X.
  • Aware of comments.
5.1.3.2 Java Parser in the TPTP Website's Service Tools
  • In Java.
  • Has a very basic example for usage.
  • Client code interacts with the parser by interfaces.
  • Quite out-of-date (according to the README).
  • Uses make to build.
  • Uses ANTLR.
5.1.3.3 OpenQED by Guy Shefner
  • In Java.
  • A personal project (no license).
  • No source code/binaries provided for now.
  • Parses a file into an internal structure.
  • For educational purpose.
  • Simply documented.
  • Unaware of comments.
  • Uses ANTLR.
5.1.3.4 marklemay/tptpParser
  • In Java.
  • Hosted on GitHub, built with maven.
  • Use Xtext (built on top of ANTLR), including the Eclipse plugin support.
  • Not sure if it is still active (last update is a year ago)
  • Little documentation.
  • Unaware of comments.