KIF syntax for Common Logic

[tillmo]

the parser is already there: CASL/fromKif.hs

[arademaker]

So I suppose that the adaptation for SUO-KIF (used in SUMO, http://www.ontologyportal.org) should not be so difficult, right?

What about translations from SUO-KIF to TPTP logic family (FOF, THF etc)? Does it make sense to implement it in Hets?

[tillmo]

Once CASL/fromKif.hs has been added as a TPTP syntax (which should be easy), the translation to TPTP, THF etc. comes for free, because such translations already exist for Common Logic.

[arademaker]

At first, the transformation from SUO-KIF to TPTP seems trivial, but SUO-KIF has many 'syntactic sugars' and @apease implemented a non-trivial transformation code in this ontology development environment SigmaKEE.

The conversion from SUO-KIF to pure FOL has the steps below. The examples were all taken from @apease's book. In collaboration with @fcbr. we have started the implementation of these steps in https://github.com/own-pt/cl-krr. I know that @apease now extended the transformation to TFF (dealing with types and arithmetic, article).

In that context, that transformation can be implemented in Hets?!

predicate variables

For all axioms that contains variables for predicates need to be consider 'templates' for formulas. So the axiom need to be instantiate for all predicates that can be valid in that context. So for

(instance part TransitiveRelation)

(<=> 
  (instance ?REL transitiveRelation)
  (=> (and
       (?REL ?I1 ?I2)
       (?REL ?I2 ?I3))
      (?REL ?I1 ?I2)))

It will be generated

(=> (and (part ?I1 ?I2)
     (part ?I1 ?I2))
    (part ?I1 ?I3))

Row variables

Some axioms contains variables starting with @. This allow a concise reference to predicates where the number of arguments are unknow.

(=> (and (subrelation ?R1 ?R2)
     (?R1 @ROW))
    (?R2 @ROW))

that would be transformed to (only showing 2 cases):

(=> (and (subrelation ?R1 ?R2)
     (?R1 ?A1))
    (?R2 ?A1))

(=> (and (subrelation ?R1 ?R2)
     (?R1 ?A1 ?A2))
    (?R2 ?A1 ?A2))

For course, this step interact with the previous one and eventually a predicate declared as binary will only be expanded to 2 arguments.

Quoting

Formulas from high-order logic have the sub-formulas quoted:

(believes John (likes Mary Jeff))

Turns to

(believes John '(likes Mary Jeff))

Effectively ignoring the subformula.

Sortals

Considering that FOL is untyped, precondictions need to be automatically added to the axiom.

(=>
 (and
  (instance ?transfer Transfer)
  (agent ?transfer ?agent)
  (patient ?transfer ?patient))
 (not (equal ?agent ?patient)))

Will be transformed into the following, adding the extra type condition for the variables ?agent and ?patient:

(=>
 (and (instance ?agent ?Agent)
      (instance ?patient Patient))
 (=>
  (and
   (instance ?transfer Transfer)
   (agent ?transfer ?agent)
   (patient ?transfer ?patient))
  (not (equal ?agent ?patient))))

[arademaker]

@eugenk can you have any documentation about the haskell code for reading Common Logic?

[eugenk]

I haven't been involved in this project for about half a decade, so my memory is a bit hazy here. As far as I remember, we only had the code and no additional documentation of parsing Common Logic in particular. Not sure if it helps: Everything related to it can be found in the CommonLogic directory.