How to use Konclude for modal logic reasoning?

[cormackikkert]

Hi,

I'm trying to run Konclude on some modal logic formula. These formula are monomodal K with converse.

I think I have a translator going, but I'm finding some formula are satisfiable, but Konclude says it is unsatisfiable. I am not sure if this is due to misunderstanding the semantics of owl ontologies, or misusing Konclude, but I was wondering if there is anything I am doing wrong?

My translator is below (with a 'small' example that is satisfiable, but Konclude says is unsatisfiable)

from lark import Lark, Transformer, v_args
modal_logic_grammar = """
start: expr
?expr: "~" expr -> not_expr
    | "(" expr ")"
    | diamond_expr
    | box_expr
    | expr "&" expr -> and_expr
    | expr "|" expr -> or_expr
    | expr "=>" expr -> implies_expr
    | expr "<=>" expr -> equiv_expr
    | TOP -> top
    | BOTTOM -> bottom
    | ID -> var_expr
diamond_expr: "<" "r" ID INVERSE? ">" expr -> diamond_expr
box_expr: "[" "r" ID INVERSE? "]" expr -> box_expr
ID: /[a-z0-9_]+/
INVERSE: "-"
TOP: "true"
BOTTOM: "false"
%import common.WS
%ignore WS
"""

class ModalLogicToOWL(Transformer):
    def __init__(self):
        self.variables = set()
        self.relations = set()

    def var_expr(self, items):
        self.variables.add(items[0])
        return f":{items[0]}"

    def not_expr(self, items):
        return f"ObjectComplementOf({items[0]})"

    def and_expr(self, items):
        return f"ObjectIntersectionOf({items[0]} {items[1]})"

    def or_expr(self, items):
        return "ObjectUnionOf({} {})".format(*items)

    def implies_expr(self, items):
        return "ObjectUnionOf(ObjectComplementOf({}) {})".format(*items)

    def equiv_expr(self, items):
        return "EquivalentClasses({} {})".format(*items)

    def diamond_expr(self, items):
        relation = f":R{items[0]}"
        self.relations.add(relation)
        if len(items) > 2 and items[1] == "-":
            relation = f"ObjectInverseOf({relation})"
        return f"ObjectSomeValuesFrom({relation} {items[-1]})"

    def box_expr(self, items):
        relation = f":R{items[0]}"
        self.relations.add(relation)
        if len(items) > 2 and items[1] == "-":
            relation = f"ObjectInverseOf({relation})"
        return f"ObjectAllValuesFrom({relation} {items[-1]})"

    def top(self, items):
        return "owl:Thing"

    def bottom(self, items):
        return "owl:Nothing"

    def multi_and_expr(self, items):
        if len(items) == 1:
            return f"{items[0]}"
        if len(items) == 2:
            return self.and_expr(items)
        else:
            return f"ObjectIntersectionOf({items[0]} {self.multi_and_expr(items[1:])})"

    def start(self, items):
        declarations = "\n".join([
            f"Declaration(Class(:D0))"] +
            [f"Declaration(Class(:{var}))" for var in self.variables] +
            [f"Declaration(ObjectProperty({rel}))" for rel in self.relations])

        owl = f"""
Prefix(:=<http://www.example.com/ontology#>)
Ontology(<http://www.example.com/ontology>
    {declarations}
    EquivalentClasses(:D0
        {self.multi_and_expr(items)}
    )
)
        """
        return owl

modal_logic_parser = Lark(modal_logic_grammar, parser='lalr', transformer=ModalLogicToOWL())
parse = modal_logic_parser.parse

def modal_to_owl(modal_str):
    return parse("("+modal_str + ")")

# Usage
example = """
(v1 | v2 | ~v3 | ([r1]([r1]~v1))) & (v1 | v4 | ~v2 | ([r1]([r1]~v1))) & (v1 | v4 | ([r1-]([r1-]v2)) | ([r1-]([r1-]~v1))) & (v1 | ~v2 | ([r1]([r1]v3)) | ([r1-]v2)) & (v2 | v3 | ([r1]([r1]v2)) | ([r1-]([r1-]v1))) & (v2 | ~v1 | ~v4 | ([r1-]([r1-]v1))) & (v2 | ~v4 | ([r1]([r1]v4)) | ([r1-]~v3)) & (v2 | ([r1-]v2) | ([r1-]~v4) | ([r1-]([r1-]v1))) & (v3 | v4 | ~v2 | ([r1-]([r1-]~v3))) & (v3 | ~v2 | ([r1]([r1]v2)) | ([r1-]([r1-]~v1))) & (v3 | ~v2 | ([r1]([r1]~v3)) | ([r1-]v3)) & (v3 | ([r1-]~v3) | ([r1-]([r1-]v1)) | ([r1-]([r1-]v2))) & (v4 | ~v1 | ([r1]([r1]~v2)) | ([r1-]([r1-]v4))) & (v4 | ([r1]~v2) | ([r1]([r1]v2)) | ([r1-]([r1-]v4))) & (~v2 | ([r1]([r1]~v1)) | ([r1]([r1]~v3)) | ([r1]([r1]~v4))) & (~v2 | ([r1]([r1]~v1)) | ([r1-]v1) | ([r1-]v2)) & (~v3 | ([r1]~v2) | ([r1]([r1]~v1)) | ([r1-]~v4)) & (~v4 | ([r1]v2) | ([r1]v4) | ([r1-]([r1-]~v2))) & (~v4 | ([r1]~v3) | ([r1-]~v2) | ([r1-]([r1-]~v3))) & (~v4 | ([r1]([r1]v3)) | ([r1-]([r1-]v3)) | ([r1-]([r1-]~v4))) & (<r1>true) & (<r1->true)
"""
if __name__ == "__main__":
    owl_str = modal_to_owl(example)
    print(owl_str)

[andreas-steigmiller]

Hi, many thanks for reporting this. It could be a bug in Konclude. Feel free to attach the generated owl file if you already have it. I will try to look into this, but, unfortunately, I do not have a lot of time at the moment. Did you double check with other reasoners (e.g. HermiT is usually very correct)?

[cormackikkert]

Good idea, I have tested with HermiT which says it is also unsatisfiable. I guess there is a problem with the translation then. Do you see any issues with the script above? I wonder if there's some misalignment going on. Or maybe is there another tried-and-true method of testing modal logic (with converse) by Konclude?

The owl file generated from the python script is here: owl.txt

[cormackikkert]

So I've actually figured out the issue, there were some operator precedence issues in the above script, which I have now fixed.

However, I'm now not sure how to handle global assumptions, is this supported?

For a concept D0 I'm trying to implement this recursively like so:

    EquivalentClasses(:D1 ObjectIntersectionOf(:D0  ObjectAllValuesFrom(:R1 :D1)))

But this is hit or miss, and works sometimes, but not with more complicated formula. Do you have any suggestions?

[andreas-steigmiller]

I'm afraid I'm not so familiar with modal logic and not completely sure what you mean with global assumption, but it sounds a bit like a restriction that should be applied for all individuals. In description logics, you can express this with owl:Thing implying something, e.g., as follows:

 SubClassOf(owl:Thing  SOME_CLASS_EXPRESSION_RESTRICTION))

I'm not sure what you intend to express with your EquivalentClasses axiom (especially since it is more related to D1 than to D0). If you say that you want to realize a restriction for a concept, then I would exect this concept in the left-hand side of the SubClassOf axiom (or directly in an EquivalentClasses axiom).

[cormackikkert]

Thanks! Sorry for not explaining but that's exactly what global assumptions are.

I'm having trouble using that expression though. Here is an example:

    Prefix(:=<http://www.example.com/ontology#>)
    Ontology(<http://www.example.com/ontology>
        Declaration(Class(:D0))
        Declaration(ObjectProperty(:R1))
        EquivalentClasses(:D0 ObjectIntersectionOf(ObjectSomeValuesFrom(:R1 owl:Thing) ObjectAllValuesFrom(:R1 ObjectAllValuesFrom(:R1 owl:Nothing)))) 
        SubClassOf(owl:Thing  :D0)
    )

It says the ontology is inconsistent:

{info} 09:36:52:722 >> Starting Konclude ...
{info} 09:36:52:722 >> Konclude - Uni Ulm Parallel Reasoner
{info} 09:36:52:722 >> Reasoner for the SROIQV(D) Description Logic, 64-bit, Version v0.7.0-1135 - 91b3e331 (Mar 16 2021)

{info} 09:36:52:723 >> Starting satisfiability checking for 'owl4.txt'.
{info} 09:36:52:723 >> Initializing reasoner. Creating calculation context.
{info} 09:36:52:723 >> Reasoner initialized with 1 processing unit(s).
{info} 09:36:52:724 >> Preprocessing ontology 'http://konclude.com/test/kb'.
{info} 09:36:52:724 >> Finished preprocessing in 0 ms for ontology 'http://konclude.com/test/kb'.
{info} 09:36:52:725 >> Precomputing ontology 'http://konclude.com/test/kb', expressiveness 'SI'.
{info} 09:36:52:725 >> Finished precomputing in 0 ms for ontology 'http://konclude.com/test/kb'.
{error} 09:36:52:725 >> 'Individual-Precomputing' processing step failed.
{error} 09:36:52:725 >> 'Consistency-Checking' processing step failed.
{error} 09:36:52:725 >> Saturation of specified concept failed.
{info} 09:36:52:725 >> Requirements for ontology 'http://konclude.com/test/kb' not satisfied.
{info} 09:36:52:725 >> Ontology 'http://konclude.com/test/kb' for Query 'UnnamedSatisfiabilityQuery' is inconsistent.
{info} 09:36:52:725 >> Ontology 'http://konclude.com/test/kb' for Query 'UnnamedSatisfiabilityQuery' is inconsistent.
{info} 09:36:52:725 >> Ontology 'http://konclude.com/test/kb' for Query 'UnnamedSatisfiabilityQuery' is inconsistent.
{error} 09:36:52:725 >> Satisfiability checking failed.

But if I remove the SubClassOf(owl:Thing :D0) line it says it is satisfiable. I think once I add this line back in the answer should be unsatisfiable.

[cormackikkert]

I'm not sure what you intend to express with your EquivalentClasses axiom (especially since it is more related to D1 than to D0). If you say that you want to realize a restriction for a concept, then I would exect this concept in the left-hand side of the SubClassOf axiom (or directly in an EquivalentClasses axiom).

I'm trying to put D1 everywhere, and saying any related individuals also have D1 and their related individuals have D1 etc, so all individuals have D1 (making D1 a global assumption in modal logic terms).

I found this works in FaCT++

(defconcept D1 (some R1 (some R1 (not (not (not (not (not *TOP*))))))))
            (defconcept D0 (and D1 (all R1 D0)))

Whereas this throws an error for Konclude:

        Prefix(:=<http://www.example.com/ontology#>)
        Ontology(<http://www.example.com/ontology>
            Declaration(Class(:D1))
            Declaration(Class(:D0))
Declaration(ObjectProperty(:R1))
            EquivalentClasses(:D1
                ObjectSomeValuesFrom(:R1 ObjectSomeValuesFrom(:R1 ObjectComplementOf(ObjectComplementOf(ObjectComplementOf(ObjectComplementOf(owl:Nothing))))))
            )
            EquivalentClasses(:D0 ObjectIntersectionOf(:D1 ObjectAllValuesFrom(:R1 D0)))
        )

[andreas-steigmiller]

I can confirm that Konclude runs into a strange exception when trying to load above ontology. But there is also a syntax error (there is a missing : before the second occurrence of D0 in the last axiom). It works for me if you load the following:

   Prefix(:=<http://www.example.com/ontology#>)
   Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
        Ontology(<http://www.example.com/ontology>
            Declaration(Class(:D1))
            Declaration(Class(:D0))
Declaration(ObjectProperty(:R1))
            EquivalentClasses(:D1
                ObjectSomeValuesFrom(:R1 ObjectSomeValuesFrom(:R1 ObjectComplementOf(ObjectComplementOf(ObjectComplementOf(ObjectComplementOf(owl:Nothing))))))
            )
            EquivalentClasses(:D0 ObjectIntersectionOf(:D1 ObjectAllValuesFrom(:R1 :D0)))
        )