=========================================
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:
Consistency check. (Reports consistency of the ontology)
Satisfiability check. (Reports if the current axiom satisfies the ontology without actually adding it.)
The core tableau reasoning procedures are written in procedural python instead of object oriented code to support optimizations and multiprocessing.
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.
ABoxAxiom(ClassAssertion(Concept("Man"),Instance("Aditya"))) TBoxAxiom(Subsumption(Concept("Man"),Concept("Biological")))KB:
[ASSERTAdityaISAMan, ALLManAREBiological]Output:
Computedmodelsare. [{'Aditya': ({'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},{Man, Biological}, True,{})}]ABoxAxiom(ClassAssertion(Concept("Man"),Instance("Aditya"))) ABoxAxiom(ClassAssertion(Concept("Machine"),Instance("Icarus"))) TBoxAxiom(Subsumption(Concept("Man"),Concept("Biological")))KB:
[ASSERTIcarusISAMachine, ASSERTAdityaISAMan, ALLManAREBiological]Output:
Computedmodelsare. [{'Aditya': ({'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},{Man, Biological}, True,{}), 'Icarus': ({'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},{NOTMan, 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,{})}]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")))KB:
[ ASSERTIcarusISAMachine, ASSERTAdityaISAMan, ALLManAREBiological, ALLMachineARENOTMan, ALLBiologicalAREMan]Output:
Computedmodelsare. [{'Aditya': ({'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},{NOTMachine, Man, Biological}, True,{}), 'Icarus': ({'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},{NOTBiological, NOTMan, Machine}, True,{})}]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")))KB:
[ ASSERTAdityaISAMan, ASSERTAdamISA (MachineANDMan), ALLManAREBiological, ALLMachineARENOTMan, ALLBiologicalAREMan]Output:
Computedmodelsare. []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")))KB:
[ ASSERTAdamISA (MachineANDMan), ASSERTAdityaISAMan, ALLManAREBiological, ALL (MachineANDMan) AREAugmented, ALLBiologicalAREMan]Output:
Computedmodelsare. [{'Adam': ({'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},{Augmented, Man, Biological, Machine}, True,{}), 'Aditya': ({'ALL': set(), 'AND': set(), 'OR': set(), 'SOME': set()},{NOTMachine, 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,{})}]