Zulip Chat Archive

Stream: new members

Topic: kif


view this post on Zulip 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.

view this post on Zulip 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))))))

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jun 21 2019 at 22:35):

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

view this post on Zulip 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