These are the expressions and axioms used by the ontologies that we want test:

Class
ClassAssertion
DataAllValuesFrom
DataProperty
DataPropertyAssertion
DataPropertyDomain
DataPropertyRange
DataSomeValuesFrom
Declaration
DifferentIndividuals
DisjointClasses
EquivalentClasses
FunctionalDataProperty
FunctionalObjectProperty
Import
InverseObjectProperties
ObjectAllValuesFrom
ObjectComplementOf
ObjectExactCardinality
ObjectHasValue
ObjectIntersectionOf
ObjectMaxCardinality
ObjectMinCardinality
ObjectOneOf
ObjectProperty
ObjectPropertyAssertion
ObjectPropertyDomain
ObjectPropertyRange
ObjectSomeValuesFrom
ObjectUnionOf
SubClassOf
SubObjectPropertyOf
SymmetricObjectProperty
TransitiveObjectProperty

Axioms such as

ClassAssertion(<http://grapson.com/expression#Noun> <http://kyamk.fi/customs/expression#zh.海关辖区.N>)
ClassAssertion(<http://grapson.com/term#Term> <http://kyamk.fi/customs/term#ru.штриховой_код.NP-kyamk.Bar_code>)

are not parsed correctly.

One of the reasoning tasks required for a OWL reasoner is check consistency. We need execute this task before classification and from the command line:

./leancor consistency tests/ontologies/examples/ontology_travel.owl ../travel-consistency.csv

The result output file () must contain ’true’ if the ontology is consistent and ’false’ if the ontology is inconsistent.

Realisation: identifying the types of all individuals in an ontology.

For realisation, the result output file () must be an OWL 2 file (in OWL 2 Functional Syntax, or any other serialization format that can be read with the OWL API), which contains all types of all individuals with ClassAssertion axioms, i.e.,

• If an individual a is an instance of a class A, then the result ontology has to contain the axiom ClassAssertion(A a), i.e., all indirect types of individuals must also be expressed by ClassAssertion axioms.
• If the ontology is inconsistent, then the result ontology must contain an axiom of the form SubClassOf(owl:Thing owl:Nothing), EquivalentClasses(owl:Thing owl:Nothing), or ClassAssertion(owl:Nothing a).

Skolemization and matrix generation are two different steps, we must reflect this in the code.

BTW, the skolemization algorithm still incomplete.

Currently we are testing if a class is subclass of all other classes, but this approach is not optimal.

This task involves finding papers related to this, e.g. https://www.cs.ox.ac.uk/files/3117/Classification.pdf, and implement or document a good solution.

We must test if the expressions and axioms are fully supported by the parser and by the matrix generator.

This task is generate an ontology using Functional Syntax with all the expressions and axioms used by wine, galen and tambis.

Grammar: http://www.w3.org/TR/owl2-syntax/#Definitions_of_OWL_2_Constructs

It's just an idea, but it would be nice if we provide an UI to visualize proofs and let easier to use the reasoner.

Some ontologies have two classes with the same name, e.g.,
SubClassOf(<http://xmlns.com/foaf/0.1/Person> <http://purl.org/dc/terms/Agent>) SubClassOf(<http://xmlns.com/foaf/0.1/Person> <http://xmlns.com/foaf/0.1/Agent>)
In this case, we get lost.

Example:

SubClassOf(<http://cui.unige.ch/isi/ontologies/citygml#chimney_(part_of_a_building)> <http://cui.unige.ch/isi/ontologies/citygml#BuildingInstallationFunctionType>)'

Create a mechanism to make queries.

http://en.wikipedia.org/wiki/Reasoning_engine

Some axioms still not supported by the parser. Most of them are commented in the code, some others need be more tested, e.g. data properties.