Home

Awesome

Athene - A description logic reasoner.

=========================================

Introduction.

Athene is a description logic reasoner written completely in native python. The current version is a beta and only supports ALC. But it can easily be extended by adding tableau rules. Athene was written with the intent of having a readable educational semantic reasoner which can be easily extended for various description logics.

Currently supported reasoning services are:

The core tableau reasoning procedures are written in procedural python instead of object oriented code to support optimizations and multiprocessing.

Tests.

Athene is still not a full feldged reasoner. For instance it does not yet support role axioms in the TBox. Below are the results of a few tests on small ontologies.

Test 1.

Ontology.
ABoxAxiom(ClassAssertion(Concept("Man"),Instance("Aditya")))
TBoxAxiom(Subsumption(Concept("Man"),Concept("Biological")))
Results.

KB:

[ASSERT Aditya IS A Man, ALL Man ARE Biological]

Output:

Computed models are.
[ { 'Aditya': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {Man, Biological},
                True,
                {})}]

Test 2.

Ontology.
ABoxAxiom(ClassAssertion(Concept("Man"),Instance("Aditya")))
ABoxAxiom(ClassAssertion(Concept("Machine"),Instance("Icarus")))
TBoxAxiom(Subsumption(Concept("Man"),Concept("Biological")))
Results.

KB:

[ASSERT Icarus IS A Machine, ASSERT Aditya IS A Man, ALL Man ARE Biological]

Output:

Computed models are.
[ { 'Aditya': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {Man, Biological},
                True,
                {}),
    'Icarus': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {NOT Man, Machine},
                True,
                {})},
  { 'Aditya': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {Man, Biological},
                True,
                {}),
    'Icarus': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {Biological, Machine},
                True,
                {})}]

Test 3.

Ontology.
ABoxAxiom(ClassAssertion(Concept("Man"),Instance("Aditya")))
ABoxAxiom(ClassAssertion(Concept("Machine"),Instance("Icarus")))
TBoxAxiom(Subsumption(Concept("Man"),Concept("Biological")))
TBoxAxiom(Subsumption(Concept("Machine"),Not(Concept("Man"))))
TBoxAxiom(Subsumption(Concept("Biological"),Concept("Man")))
Results.

KB:

[ ASSERT Icarus IS A Machine,
  ASSERT Aditya IS A Man,
  ALL Man ARE Biological,
  ALL Machine ARE NOT Man,
  ALL Biological ARE Man]

Output:

Computed models are.
[ { 'Aditya': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {NOT Machine, Man, Biological},
                True,
                {}),
    'Icarus': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {NOT Biological, NOT Man, Machine},
                True,
                {})}]

Test 4.

Ontology.

ABoxAxiom(ClassAssertion(Concept("Man"),Instance("Aditya")))
ABoxAxiom(ClassAssertion(And(Concept("Machine"),Concept("Man")),Instance("Adam")))
TBoxAxiom(Subsumption(Concept("Man"),Concept("Biological")))
TBoxAxiom(Subsumption(Concept("Machine"),Not(Concept("Man"))))
TBoxAxiom(Subsumption(Concept("Biological"),Concept("Man")))
Results.

KB:

[ ASSERT Aditya IS A Man,
  ASSERT Adam IS A (Machine AND Man),
  ALL Man ARE Biological,
  ALL Machine ARE NOT Man,
  ALL Biological ARE Man]

Output:

Computed models are.
[]

Test 5.

Ontology.
ABoxAxiom(ClassAssertion(Concept("Man"),Instance("Aditya")))
ABoxAxiom(ClassAssertion(And(Concept("Machine"),Concept("Man")),Instance("Adam")))
TBoxAxiom(Subsumption(Concept("Man"),Concept("Biological")))
TBoxAxiom(Subsumption(Concept("Biological"),Concept("Man")))
TBoxAxiom(Subsumption(And(Concept("Machine"),Concept("Man")),Concept("Augmented")))
Results.

KB:

[ ASSERT Adam IS A (Machine AND Man),
  ASSERT Aditya IS A Man,
  ALL Man ARE Biological,
  ALL (Machine AND Man) ARE Augmented,
  ALL Biological ARE Man]

Output:

Computed models are.
[ { 'Adam': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
              {Augmented, Man, Biological, Machine},
              True,
              {}),
    'Aditya': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {NOT Machine, Man, Biological},
                True,
                {})},
  { 'Adam': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
              {Augmented, Man, Biological, Machine},
              True,
              {}),
    'Aditya': ( {'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},
                {Augmented, Man, Biological},
                True,
                {})}]