A recent MSc thesis at IFI explored how to add "Epsilon nominals" to a Description Logic. Simply speaking, if KingOfFrance is the concept describing all kings of France, then the epsilon nominal εKingOfFrance denotes "A king of France" (at least as long as there is a king of France)
This work was very successful, but some things remain to be done that can be part of a MSc thesis:
- We would like to have an implementation. It is extremely challenging to implement a theorem prover from scratch, so the idea would be to start from an existing theorem prover and extend it with epsilon nominals.
- Depending on the choice of the theorem prover to extend, some theoretical work may be needed to "bridge the gap" between the approach in the previous thesis and the theorem prover.
- Apart from implementation-oriented tasks, there are also some theoretical questions that remain open.