How ontologies like SUMO can be represented in dependent types systems like Lean?

We are developing a knowledge base in a dependent types system called Lean, based on SUMO. The current aim of the project is to develop a package containing axioms and definitions, describing common sense, alongside Lean automation power, to solve common sense logical problems.

It’s possible to install locally the package, so that scratch files, that are not in a package, can use its dependencies. You should clone or download the project, and then, install by typing

git clone https://github.com/own-pt/common-sense-lean.git
cd common-sense-lean
leanpkg install cs-lib

If you have already the repository locally, just go to the directory and type the last command. It creates a reference in ~/.lean/leanpkg.toml for the package to be accessed from the other files.

For details about Lean packages, see Using the Package Manager.

• http://www.ontologyportal.org
• http://leanprover.github.io
• http://tptp.org/Challenges/SUMOChallenge/
• http://tptp.org