SUMO to TPTP conversion

Predicate variables

relation conversion

Consider the transitive relation:

(=>
  (instance ?R TransitiveRelation)
  (=>
    (and
      (?R ?A ?B)
      (?R ?B ?C))
    (?R ?A ?C)))

Consider a particular relation:

(instance part TransitiveRelation)

A pre-processor will create a new axiom based on the above anytime a new relation (like part) is instantiated as a new TransitiveRelation.

(=>
  (and
   (part ?A ?B)
   (part ?B ?C))
  (part ?A ?C))

This is done for all similar relations.

Row variables

partition

A partition statement is an exhaustive dividing of a set.

For example, Major League Baseball teams can ALL be divided into National League, or American League teams with no teams left over.

(partition MajorLeagueTeams NationalLeagueTeams AmericanLeagueTeams)

The partition relation is tricky, because there is not a fixed number of inputs. "Communication" for example is partitioned into 6 different entities.

In SUMO we handle this with Row Variables.

(=>
  (partition @ROW)
  (and
    (exhaustive @ROW)
    (disjoint @ROW)))

The @ROW is a row variable, and means that there are any number of inputs to the partition relation.

TPTP does not have the concept of the row variable, so when converting SUMO to TPTP, different partition relations are automatically generated to cover the breadth of partitions possible in SUMO. i.e.

(partition_1 ?ARG1)
(partition_2 ?ARG1 ?ARG2)
...
(partition_6 ?ARG1 ... ?ARG6)

Type guards

TPTP FOF is an untyped language. In SUMO we WANT things to be restricted by type. For example (part ?A ?B), we want ?A and ?B to be restricted to objects. We don't want a number to be a part of an object to be an abstract thing, like a number. Like this: (part 3 MyRightShoe). SUMO will catch this and restrict it with type guards.

Type restrictions are created with domain and range preconditions on axioms.

(domain part 1 Object)
(domain part 2 Object)

When converting to TPTP, SUMO is automatically generated ...

Translation to TFF

In TFF we have the following types:

$o - boolean
$RAT - rational number
$REAL - real number
$INT - integer
$i - everything else
$TTYPE - custom types

TFF does not have multiple inheritance however which makes things tricky. PositiveInteger in SUMO for example, has to be hand coded in TFF.