Inference engine for satisfiability in ALC
I was analyzing papers on the web for an academic project when I realized that the state of art about the concept satisfiability in Description Logics (DL) is poor a bit. Since I learn constantly from open discussions (a special thanks goes to Medium), I completely approve the dissemination of interesting problems. Thus, I want to do my share.
It all began because my friend (Salvatore Amodio) and I had to build up from scratch an inference engine based on Tableau Method in order to query it with a concept written in ALC and wait for satisfiability response. The reasoner had to consider a not empty TBox and a computation speed up technique. These requirements forced us to implement:
- Blocking
- Lazy Unfolding
The former is necessary for reasoning decidability, while the latter is taken from the suite of optimization technique (e.g. Semantic branching, DDB).
Project’s structure
The following is the simplified project’s structure that should give a comprehensive overview.
The core class which contains the tableau algorithm, the blocking technique, the lazy unfolding and all the elements for the inference engine is Reasoner.java . The main class used to start the program is IOParser.java. Finally, the last one is for visualizing the result as graph and RDF.
Run setup
After the insertion of your ontology in ontologies/ directory, few lines of code are necessary in order to make everything work.
After that, you have only to run the program.
Use case
Just to give an example, suppose you have written an easy ontology based on food. It contains trivial axioms such as domain/range definition and GCI (General Concept Inclusions).
Once formalized the ontology (e.g. in Manchester Syntax), you can put it in ontologies/ directory of the project. When you run the program, a GUI will appear waiting for the user input, namely a concept written in Manchester Syntax.
The entities in the concept are mapped to the ontology. Particularly, you should write the entities with the full name, like <http://owl.api.tutorial#Person>, or with the prefix, like t:Person (if Prefix: t: <http://owl.api.tutorial#> is in the ontology). You can eventually save or open a txt file containing the concept always written in Manchester Syntax.
Supposing you write it correctly, the button “Done” generates two dialogs saying that the concept is translated with OWL API classes and that the inference engine started the processing. Afterwards you have the result. For instance, with the respect to the food-based ontology considered before, a concept t:Person creates the following tableau visualized as tree:
The dashed edge indicates the concepts that the individual must satisfy. The blue rectangle means that the concepts come from the application of Lazy Unfolding rules (if the content is the same as the normal rectangle, lazy unfolding rules are applied but no one of new concept is inserted). The red node notices the presence of a clash, while the green one highlights the query concept satisfiability. The graph is eventually accompanied with RDF file in Turtle notation located in result/ directory.
Finally, the terminal presents some prints in order to enrich the result.
------ TABLEAUX METHOD FOR SAT IN ALC ------INPUT CONCEPT:
<http://owl.api.tutorial#Person>[Time passed: 42ms] Concept satisfiability: Yes
I leave the link to the github project here below. Hope it is inspirational or kind of useful.
