kif

Stream: new members

[Alexandre Rademaker]

I am playing with SUMO ontology (http://ontologyportal.org ) trying to understand its semantics and possible translation to dependent types.

[Alexandre Rademaker]

one of the language features is the use of row variables (a way to deal with variable arity). So a variable with an @, in the beginning, means a placeholder to one or more arguments. The axiom below, use ListFn (constructor of lists given any number of arguments, the equivalent of Common Lisp list function) and inList to check if an item is an element of the list. How to translate it to Lean?

(=>
   (exhaustiveDecomposition ?CLASS @ROW)
   (forall (?OBJ)
       (=>
           (instance ?OBJ ?CLASS)
           (exists (?ITEM)
               (and
                   (inList ?ITEM (ListFn @ROW))
                   (instance ?OBJ ?ITEM))))))

[Kevin Buzzard]

The SUMO guy (Adam Pease) spoke at AITP this year: aitp-conference.org/2019/slides/AP.pdf

[Alexandre Rademaker]

yep! I am planning to work with him in the formalization of the translation from SUMO to TF0.

[Bryan Gin-ge Chen]

What do you mean by "translate it to Lean" exactly?

[Alexandre Rademaker]

Good question. I am still thinking about the details, but I am trying something like:

R. Dapoigny and P. Barlatier, “Formalizing Context for Domain Ontologies in Coq,”, May 2014.

All axioms could be encoded as variables, right? For example, the SUMO axiom (simplified):

(<=>
    (partition ?class ?x ?y)
    (and
        (exhaustiveDecomposition ?class ?x ?y)
        (disjointDecomposition ?class ?x ?y)))

could be encoded as:

constant Class : Type

constants partition exhaustiveDecomposition disjointDecomposition :
 Class → Class → Class → Prop

variable AxPartition : ∀ x y z : Class,
 partition x y z ↔ exhaustiveDecomposition x y z ∧ disjointDecomposition x y z

Does it make sense?