Model generation

[Martin Strecker]

Hi, 

I wonder whether Hermit can be used in a "model generation" mode - something a typical SAT / SMT solver would do. More precisely, given a TBox and an ABox, can Hermit generate a model (in the form of a Kripke structure) provided the conjuction of TBox and ABox is satisfiable? How to access this model?

In a similar stance, but more concretely: I am currently experimenting with Hermit via its Protégé interface. I wonder how one can display instances of a class that are existentially asserted (thus in the form of Skolem constants / anonymous individuals) without being named individuals.

Sorry for my maybe naive question, but I haven't found an answer in the Hermit / Protégé documentation.

Thanks in advance,

Martin Strecker

[Birte Glimm]

Hi Martin,

HermiT generates model abstractions that are not full models. Since
many DLs do not enjoy the finite model properties, HermiT uses
blocking techniques to check for cyclic expansions, which are then
blocked and not further continued. It can theoretically be guaranteed
that such model abstraction can be expanded into (infinite) models.
Hence, HermiT can at most produce the generated model abstractions. At
the moment, you can use the HermiT debugger to see the generated model
abstraction. There is no command line interface for this. The HermiT
examples include HermiTDebugger.java (see also attachment), which
shows some examples of how the debugger can be used.

Best, Birte

> --
> You received this message because you are subscribed to the Google Groups "HermiT Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hermit-users...@googlegroups.com.
> To view this discussion on the web, visit https://groups.google.com/d/msgid/hermit-users/61ae1fb6-8b18-4941-8010-b8f31f09878en%40googlegroups.com.



--
Prof. Dr. Birte Glimm Tel.: +49 731 50 24125
Inst. of Artificial Intelligence Secr: +49 731 50 24258
University of Ulm Fax: +49 731 50 24188
D-89069 Ulm birte...@uni-ulm.de
Germany