## Stream: new members

### Topic: kif

#### Alexandre Rademaker (Jun 21 2019 at 22:05):

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

#### Alexandre Rademaker (Jun 21 2019 at 22:08):

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 (Jun 21 2019 at 22:08):

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

#### Alexandre Rademaker (Jun 21 2019 at 22:09):

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

#### Bryan Gin-ge Chen (Jun 21 2019 at 22:35):

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

#### Alexandre Rademaker (Jun 22 2019 at 03:10):

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?

Last updated: May 14 2021 at 13:24 UTC