OWL Top Level Classes

@dataclass
class OntologyElement:
    """
    A class or property.

    Note this is designed to simulate python classes, such that it can be used in place
    of Thing, TopObjectProperty, TopDataProperty, etc.
    """

    __name__: OntologyElementReference
    owl_type: Optional[str] = None
    iri: Optional[IRI] = None

    def __str__(self):
        # return f"{self.owl_type}({self.__name__})"
        return self.__name__

    def __repr__(self):
        if self.iri:
            return f"{self.owl_type}({self.__name__}, {self.iri})"
        else:
            return f"{self.owl_type}({self.__name__})"

@dataclass(frozen=True)
class Thing(Fact):
    """
    The top level class in OWL-DL. Everything is a Thing.

    For your object model to be included in the OWL-DL mapping, all your classes
    representing individuals should inherit from Thing.

    Basic Example:

    ```python
    class Person(Thing):
        '''A person'''

    class Pet(Thing):
        '''A pet'''
    ```

    Formally, OWL Classes are unary predicates, and instances are unary ground terms:

    ```python
    facts = [Person("P1"), Pet("Fido")]
    ```

    You can create more complex defined classes, using OWL Frame-style class definitions:

    ```python
    class HasPet(TopObjectProperty):
        '''A property that relates a person to a pet'''
        domain = Person
        range = Pet

    class PetOwner(Person):
        '''A person that owns a pet'''
        equivalent_to = Person & ObjectSomeValuesFrom(HasPet, Pet)
    ```

    A thing class can have ClassVars `equivalent_to`, `subclass_of`, ...
    Note these are class-level.

    We can create and reason over instances and facts:

    ```python
    facts = [Person("P1"), Pet("Fido"), HasPet("P1", "Fido")]
    reasoner = OWLReasoner()
    reasoner.init_from_file(Path(__file__))
    for f in facts:
        reasoner.add(f)
    model = reasoner.model()
    for t in model.ground_terms:
        print(t)
    ```

    Results will include:

    ```
    PetOwner(P1)
    ```

    Formally, the Thing class is a subclass of a typed-logic Fact, which instantiates an
    OWLCLass python metaclass:

    ```mermaid
    classDiagram
    class Thing {
        IRI iri
    }
    Fact <|-- Thing
    Thing --> `OWLCLass[[metaclass]]` : instance_of
    `OWLCLass[[metaclass]]` --> "*" ClassExpression : subclass_of
    `OWLCLass[[metaclass]]` --> "*" ClassExpression : equivalent_to
    `OWLCLass[[metaclass]]` --> "*" ClassExpression : disjoint_with
    `OWLCLass[[metaclass]]` --> "*" ClassExpression : disjoint_union_of
    ```

    """

    iri: IRI

    subclass_of: ClassVar[Optional["ClassExpression"]] = None
    equivalent_to: ClassVar[Optional["ClassExpression"]] = None
    disjoint_with: ClassVar[Optional["ClassExpression"]] = None
    disjoint_union_of: ClassVar[Optional[List["ClassExpression"]]] = None

    @classmethod
    def axioms_iter(cls) -> Iterator["Axiom"]:
        for parent in cls.__bases__:
            if issubclass(parent, Thing):
                yield SubClassOf(cls, parent)
        yield from [SubClassOf(cls, e) for e in as_list(cls.subclass_of)]
        yield from [DisjointClasses(cls, e) for e in as_list(cls.disjoint_with)]
        yield from [EquivalentClasses(cls, e) for e in as_list(cls.equivalent_to)]
        if cls.disjoint_union_of:
            yield DisjointUnion(cls, *cls.disjoint_union_of)

    @classmethod
    def axioms(cls) -> List["Axiom"]:
        return list(cls.axioms_iter())

    @classmethod
    def to_sentences(cls) -> List[Sentence]:
        return [a for a in [axiom.as_fol() for axiom in cls.axioms()] if a is not None]

@dataclass(frozen=True)
class TopObjectProperty(Fact):
    """
    The top object property.

    Example:
    -------
    ```python
    class Person(Thing):
        '''A person'''

    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    class HasAncestor(HasParent):
        '''A property that relates a person to their ancestor'''
        transitive = True
    ```

    Formally, OWL Object Properties are binary predicates, and instances are binary ground terms:

    ```python
    facts = [HasParent("P1", "P2"), HasAncestor("P1", "P3")]
    ```

    Formally, the TopObjectProperty class is a subclass of a 2-ary typed-logic Fact, which instantiates an
    OWLObjectProperty python metaclass:

    ```mermaid
    classDiagram
    class TopObjectProperty {
        IRI subject
        IRI object
    }
    Fact <|-- TopObjectProperty
    TopObjectProperty --> `OWLObjectProperty[[metaclass]]` : instance_of
    `OWLObjectProperty[[metaclass]]` --> "*" ObjectPropertyExpression : subproperty_of
    `OWLObjectProperty[[metaclass]]` --> "*" PropertyExpressionChain : subproperty_chain
    `OWLObjectProperty[[metaclass]]` --> "*" ClassExpression : domain
    `OWLObjectProperty[[metaclass]]` --> "*" ClassExpression : range

    class `OWLObjectProperty[[metaclass]]` {
       Boolean transitive
       Boolean symmetric
       Boolean asymmetric
       Boolean reflexive
      Boolean irreflexive
      Boolean functional
      Boolean inverse_functional
    }
    ```



    """

    subject: IRI
    object: IRI

    transitive: ClassVar[Optional[bool]] = None
    symmetric: ClassVar[Optional[bool]] = None
    asymmetric: ClassVar[Optional[bool]] = None
    reflexive: ClassVar[Optional[bool]] = None
    irreflexive: ClassVar[Optional[bool]] = None
    functional: ClassVar[Optional[bool]] = None
    inverse_functional: ClassVar[Optional[bool]] = None
    subproperty_of: ClassVar[Optional["ObjectPropertyExpression"]] = None
    subproperty_chain: ClassVar[Optional["PropertyExpressionChain"]] = None
    equivalent_to: ClassVar[Optional["ObjectPropertyExpression"]] = None
    disjoint_with: ClassVar[Optional["ObjectPropertyExpression"]] = None
    inverse_of: ClassVar[Optional["ObjectPropertyExpression"]] = None
    domain: ClassVar[Optional["ClassExpression"]] = None
    range: ClassVar[Optional["ClassExpression"]] = None

    @classmethod
    def some(cls, ce: "ClassExpression") -> "ObjectSomeValuesFrom":
        return ObjectSomeValuesFrom(cls, ce)

    @classmethod
    def only(cls, ce: "ClassExpression") -> "ObjectAllValuesFrom":
        return ObjectAllValuesFrom(cls, ce)

    @classmethod
    def value(cls, i: "Individual") -> "ObjectHasValue":
        return ObjectHasValue(cls, i)

    @classmethod
    def axioms_iter(cls) -> Iterator["Axiom"]:
        for parent in cls.__bases__:
            if issubclass(parent, TopObjectProperty):
                yield SubObjectPropertyOf(cls, parent)
        yield from [SubObjectPropertyOf(cls, e) for e in as_list(cls.subproperty_of)]
        yield from [SubObjectPropertyOf(chain, cls) for chain in as_list(cls.subproperty_chain)]
        yield from [ObjectPropertyDomain(cls, e) for e in as_list(cls.domain)]
        yield from [ObjectPropertyRange(cls, e) for e in as_list(cls.range)]
        if cls.transitive:
            yield from [TransitiveObjectProperty(cls)]
        if cls.symmetric:
            yield from [SymmetricObjectProperty(cls)]
        if cls.asymmetric:
            yield from [AsymmetricObjectProperty(cls)]
        if cls.reflexive:
            yield from [ReflexiveObjectProperty(cls)]
        if cls.irreflexive:
            yield from [IrreflexiveObjectProperty(cls)]
        if cls.functional:
            yield from [FunctionalObjectProperty(cls)]
        if cls.inverse_functional:
            yield from [InverseFunctionalObjectProperty(cls)]
        yield from [EquivalentObjectProperties(cls, e) for e in as_list(cls.equivalent_to)]
        yield from [DisjointObjectProperties(cls, e) for e in as_list(cls.disjoint_with)]
        if cls.inverse_of:
            yield from [InverseObjectProperties(cls, cls.inverse_of)]

    @classmethod
    def axioms(cls) -> List["Axiom"]:
        return list(cls.axioms_iter())

    @classmethod
    def to_sentences(cls) -> List[Sentence]:
        return [a for a in [axiom.as_fol() for axiom in cls.axioms()] if a is not None]

@dataclass(frozen=True)
class TopDataProperty(Fact):
    """
    The top data property.

    Example:
    -------
    ```python
    class Person(Thing):
        '''A person'''

    class HasAge(TopDataProperty):
        '''A property that relates a person to their age'''
        domain = Person
        range = int
    ```

    Formally, OWL Data Properties are binary predicates, and instances are binary ground terms:

    ```python
    facts = [HasAge("P1", 25)]
    ```

    Formally, the TopDataProperty class is a subclass of a 2-ary typed-logic Fact, which instantiates an
    OWLDataProperty python metaclass:

    ```mermaid
    classDiagram
    class TopDataProperty {
        IRI subject
        Union[str, int, float, bool, Decimal] object
    }
    Fact <|-- TopDataProperty
    TopDataProperty --> `OWLDataProperty[[metaclass]]` : instance_of
    `OWLDataProperty[[metaclass]]` --> "*" DataPropertyExpression : subproperty_of
    `OWLDataProperty[[metaclass]]` --> "*" ClassExpression : domain
    `OWLDataProperty[[metaclass]]` --> "*" DataRange : range
    class `OWLDataProperty[[metaclass]]` {
         Boolean functional
     }
     ```

    """

    subject: IRI
    object: Union[str, int, float, bool, Decimal]

    functional: ClassVar[Optional[bool]] = None
    subproperty_of: ClassVar[Optional["DataPropertyExpression"]] = None
    equivalent_to: ClassVar[Optional["DataPropertyExpression"]] = None
    disjoint_with: ClassVar[Optional["DataPropertyExpression"]] = None
    domain: ClassVar[Optional["ClassExpression"]] = None
    range: ClassVar[Optional["DataRange"]] = None

    @classmethod
    def axioms_iter(cls) -> Iterator["Axiom"]:
        for parent in cls.__bases__:
            if issubclass(parent, TopDataProperty):
                yield SubDataPropertyOf(cls, parent)
        yield from [SubDataPropertyOf(cls, e) for e in as_list(cls.subproperty_of)]
        yield from [DataPropertyDomain(cls, e) for e in as_list(cls.domain)]
        yield from [DataPropertyRange(cls, e) for e in as_list(cls.range)]
        if cls.functional:
            yield from [FunctionalDataProperty(cls)]
        yield from [EquivalentDataProperties(cls, e) for e in as_list(cls.equivalent_to)]
        yield from [DisjointDataProperties(cls, e) for e in as_list(cls.disjoint_with)]

    @classmethod
    def axioms(cls) -> List["Axiom"]:
        return list(cls.axioms_iter())

    @classmethod
    def to_sentences(cls) -> List[Sentence]:
        return [a for a in [axiom.as_fol() for axiom in cls.axioms()] if a is not None]

@dataclass
class AnonymousIndividual(ABC):
    """
    An anonymous individual.
    """

    first: str

@dataclass
class Literal(ABC):
    """
    A literal.
    """

    pass

@dataclass
class SimpleLiteral:
    """
    A simple literal.
    """

    literal: str

@dataclass
class LanguageLiteral:
    """
    A language literal.

    Example:

        >>> v = LanguageLiteral("fromage", "en")
    """

    literal: str
    lang: str

@dataclass
class DatatypeLiteral:
    """
    A datatype literal.

    Example:

        >>> v = LanguageLiteral("12", "xsd:int")
    """

    literal: str
    datatype_iri: IRI

@dataclass
class Axiom(ABC):
    """
    Abstract base class for axioms.

    Axioms can be declared implicitly, in "Frame-style" class definitions, or in
    an `__axioms__` module variable
    """

    frame_keyword: ClassVar[Optional[str]] = None
    annotations: ClassVar[Optional[Mapping[str, Any]]] = None

    # @abstractmethod
    def as_fol(self) -> Optional[Sentence]:
        return None

@dataclass
class SubClassOf(Axiom):
    """
    A sub-class-of axiom.

    Axioms can be declared explicitly:

    ```python
    class Person(Thing):
        '''A person'''

    class Employee(Thing):
        '''A person that is employed'''

    __axioms__ = [ SubClassOf(Employee, Person) ]
    ```

    However, it is more idiomatic to declare axioms implicitly in Frame-style class definitions:

    ```python
    class Person(Thing):
        '''A person'''

    class Employee(Thing):
        '''A person that is employed'''
        subclass_of = Person
    ```

    Note that when the superclass is a named class, the more pythonic equivalent is preferred:

    ```python
    class Employee(Person):
        '''A person that is employed'''
    ```

    Using an explicit class var is necessary when the superclass is an expression:

    ```python
    class Organization(Thing):
        '''An organization'''

    class EmployedBy(TopObjectProperty):
        domain = Employee
        range = Organization

    class Employee(Person):
        '''A person that is employed'''
        subclass_of = ObjectSomeValuesFrom(EmployedBy, Organization)
    ```

    UML:

    ```mermaid
    classDiagram
    AnonymousClassExpression <|-- SubClassOf
    SubClassOf --> "*" ClassExpression : sub
    SubClassOf --> "*" ClassExpression : sup
    ```

    """

    frame_keyword = "subclass_of"
    sub: ClassExpression
    sup: ClassExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall([I], Implies(instance_of(I, self.sub), instance_of(I, self.sup)))

    def __repr__(self) -> str:
        return f"SubClassOf({self.sub}, {self.sup})"

@dataclass
class PropertyExpressionChain:
    """
    A chain of property expressions.

    Example:
    -------
    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    class HasGrandparent(TopObjectProperty):
        '''A property that relates a person to their grandparent'''
        subproperty_chain = PropertyExpressionChain(HasParent, HasParent)
    ```

    UML:

    ```
    classDiagram
    PropertyExpressionChain --> "*" ObjectPropertyExpression : chain
    ```

    """

    chain: Tuple[ObjectPropertyExpression, ...]

    def __init__(self, *chain: ObjectPropertyExpression):
        self.chain = chain

@dataclass
class SubObjectPropertyOf(Axiom):
    """
    A sub-object-property-of axiom.

    Example of explicit declaration:

    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    class HasGrandparent(TopObjectProperty):
        '''A property that relates a person to their grandparent'''

    __axioms__ = [ SubObjectPropertyOf(HasGrandparent, HasParent) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    class HasGrandparent(TopObjectProperty):
        '''A property that relates a person to their grandparent'''
        subproperty_of = HasParent
    ```

    When the parent is a named class, the more pythonic equivalent is preferred:

    ```python
    class HasGrandparent(HasParent):
        '''A property that relates a person to their grandparent'''
    ```

    UML:

    ```mermaid
    classDiagram
    AnonymousClassExpression <|-- SubObjectPropertyOf
    SubObjectPropertyOf --> "*" ObjectPropertyExpressionOrPropertyExpressionChain : sub
    SubObjectPropertyOf --> "*" ObjectPropertyExpression : sup
    ```

    """

    frame_keyword = "subproperty_of"
    sub: Union[ObjectPropertyExpression, PropertyExpressionChain]
    sup: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        if isinstance(self.sup, PropertyExpressionChain):
            raise ValueError(f"Cannot have a chain as a super property - did you accidentally invert? {self}")
        if isinstance(self.sub, PropertyExpressionChain):
            chain_len = len(self.sub.chain)
            inst_vars = [Variable(f"J{i}") for i in range(chain_len + 1)]
            conjs = []
            for i in range(chain_len):
                conjs.append(instance_of_op(inst_vars[i], inst_vars[i + 1], self.sub.chain[i]))
            return Forall(inst_vars, Implies(And(*conjs), instance_of_op(inst_vars[0], inst_vars[-1], self.sup)))
        else:
            return Forall([P, I, J], Implies(instance_of_op(I, J, self.sub), instance_of_op(I, J, self.sup)))

@dataclass
class TransitiveObjectProperty(Axiom):
    """
    A transitive-object-property axiom.

    Example of explicit declaration:

    ```python
    class HasAncestor(TopObjectProperty):
        pass

    __axioms__ = [ TransitiveObjectProperty(HasAncestor) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasAncestor(TopObjectProperty):
        transitive = True
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- TransitiveObjectProperty
    TransitiveObjectProperty --> "1" ObjectPropertyExpression : first
    ```

    """

    frame_keyword = "transitive"
    first: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall(
            [I, J, K],
            Implies(
                And(instance_of_op(I, J, self.first), instance_of_op(J, K, self.first)),
                instance_of_op(I, K, self.first),
            ),
        )

@dataclass
class InverseObjectProperties(Axiom):
    """
    An inverse-object-properties axiom.

    Example of explicit declaration:

    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    class HasChild(TopObjectProperty):
        '''A property that relates a person to their child'''
        domain = Person
        range = Person

    __axioms__ = [ InverseObjectProperties(HasParent, HasChild) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person
        inverse_of = HasChild
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- InverseObjectProperties
    InverseObjectProperties --> "1" ObjectPropertyExpression : first
    InverseObjectProperties --> "1" ObjectPropertyExpression : second
    ```
    """

    frame_keyword = "inverse_of"
    first: ObjectPropertyExpression
    second: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall([I, J], Iff(instance_of_op(I, J, self.first), instance_of_op(J, I, self.second)))

@dataclass
class SymmetricObjectProperty(Axiom):
    """
    A symmetric-object-property axiom.

    Example of explicit declaration:

    ```python
    class HasSibling(TopObjectProperty):
        '''A property that relates a person to their sibling'''
        domain = Person
        range = Person

    __axioms__ = [ SymmetricObjectProperty(HasSibling) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasSibling(TopObjectProperty):
        '''A property that relates a person to their sibling'''
        domain = Person
        range = Person
        symmetric = True
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- SymmetricObjectProperty
    SymmetricObjectProperty --> "1" ObjectPropertyExpression : first
    ```

    """

    frame_keyword = "symmetric"
    first: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall([I, J], Iff(instance_of_op(I, J, self.first), instance_of_op(J, I, self.first)))

@dataclass
class AsymmetricObjectProperty(Axiom):
    """
    An asymmetric-object-property axiom.

    Example of explicit declaration:

    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    __axioms__ = [ AsymmetricObjectProperty(HasParent) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person
        asymmetric = True
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- AsymmetricObjectProperty
    AsymmetricObjectProperty --> "1" ObjectPropertyExpression : first
    ```

    """

    frame_keyword = "asymmetric"
    first: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall([I, J], Implies(instance_of_op(I, J, self.first), Not(instance_of_op(J, I, self.first))))

@dataclass
class ReflexiveObjectProperty(Axiom):
    """
    A reflexive-object-property axiom.

    Example of explicit declaration:

    ```python
    class RelatedTo(TopObjectProperty):
        '''A property that relates a thing to itself'''
        domain = Thing
        range = Thing

    __axioms__ = [ ReflexiveObjectProperty(RelatedTo) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class RelatedTo(TopObjectProperty):
        '''A property that relates a thing to itself'''
        domain = Thing
        range = Thing
        reflexive = True
    ```

    In practice, relfexive axioms are too strong, but we include them for completeness.

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- ReflexiveObjectProperty
    ReflexiveObjectProperty --> "1" ObjectPropertyExpression : first
    ```

    """

    frame_keyword = "reflexive"
    first: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall([I, C], Implies(instance_of(I, Thing), instance_of_op(I, I, self.first)))

@dataclass
class IrreflexiveObjectProperty(Axiom):
    """
    An irreflexive-object-property axiom.

    Example of explicit declaration:

    ```python

    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    __axioms__ = [ IrreflexiveObjectProperty(HasParent) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person
        irreflexive = True
    ```

    """

    frame_keyword = "irreflexive"
    first: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        refl_s = instance_of_op(I, I, self.first)
        if refl_s:
            return Not(Exists([I], refl_s))
        return None

@dataclass
class FunctionalObjectProperty(Axiom):
    """
    A functional-object-property axiom.

    Example of explicit declaration:

    ```python

    class HasBiologicalMother(TopObjectProperty):
        '''A property that relates a person to their biological mother'''
        domain = Person
        range = Person

    __axioms__ = [ FunctionalObjectProperty(HasBiologicalMother) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasBiologicalMother(TopObjectProperty):
        '''A property that relates a person to their biological mother'''
        domain = Person
        range = Person
        functional = True
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- FunctionalObjectProperty
    FunctionalObjectProperty --> "1" ObjectPropertyExpression : first
    ```

    """

    frame_keyword = "functional"
    first: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall(
            [I, J, K],
            Implies(And(instance_of_op(I, J, self.first), instance_of_op(I, K, self.first)), Term("eq", J, K)),
        )

@dataclass
class InverseFunctionalObjectProperty(Axiom):
    """
    An inverse-functional-object-property axiom.

    Example of explicit declaration:

    ```python
    class BiologicalMotherOf(TopObjectProperty):
        '''A property that relates a person to their biological mother'''
        domain = Person
        range = Person

    __axioms__ = [ InverseFunctionalObjectProperty(BiologicalMotherOf) ]

    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class BiologicalMotherOf(TopObjectProperty):
        '''A property that relates a person to their biological mother'''
        domain = Person
        range = Person
        inverse_functional = True
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- InverseFunctionalObjectProperty
    InverseFunctionalObjectProperty --> "1" ObjectPropertyExpression : first
    ```
    """

    frame_keyword = "inverse_functional"
    first: ObjectPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall(
            [I, J, K],
            Implies(And(instance_of_op(I, J, self.first), instance_of_op(K, J, self.first)), Term("eq", I, K)),
        )

@dataclass
class FunctionalDataProperty(Axiom):
    """
    A functional-data-property axiom.

    Example of explicit declaration:

    ```python
    class HasAge(TopDataProperty):
        '''A property that relates a person to their age'''
        domain = Person
        range = int

    __axioms__ = [ FunctionalDataProperty(HasAge) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasAge(TopDataProperty):
        '''A property that relates a person to their age'''
        domain = Person
        range = int
        functional = True
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- FunctionalDataProperty
    FunctionalDataProperty --> "1" DataPropertyExpression : first
    ```

    """

    frame_keyword = "functional"
    first: DataPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall(
            [I, J, K],
            Implies(And(instance_of_dp(I, J, self.first), instance_of_dp(I, K, self.first)), Term("eq", J, K)),
        )

@dataclass
class SubDataPropertyOf(Axiom):
    """
    A sub-data-property-of axiom.

    Example of explicit declaration:

    ```python
    class HasAge(TopDataProperty):
        '''A property that relates a thing to their age'''
        range = int

    class PersonAge(TopDataProperty):
        '''A property that relates a person to their age'''
        domain = Person

    __axioms__ = [ SubDataPropertyOf(PersonAge, HasAge) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class PersonAge(TopDataProperty):
        '''A property that relates a person to their age'''
        domain = Person
        range = int
        subproperty_of = HasAge
    ```

    When the parent is a named class, the more pythonic equivalent is preferred:

    ```python
    class PersonAge(HasAge):
        '''A property that relates a person to their age'''
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- SubDataPropertyOf
    SubDataPropertyOf --> "*" DataPropertyExpression : sub
    SubDataPropertyOf --> "*" DataPropertyExpression : sup
    ```
    """

    frame_keyword = "subproperty_of"
    sub: DataPropertyExpression
    sup: DataPropertyExpression

    def as_fol(self) -> Optional[Sentence]:
        return Forall([P, I, J], Implies(instance_of_dp(I, J, self.sub), instance_of_dp(I, J, self.sup)))

@dataclass
class EquivalentClasses(Axiom):
    """
    An equivalent-classes axiom.

    Example of explicit declaration:

    ```python
    class Food(Thing):
        pass

    class Beverage(Thing):
        pass

    class MenuItem(Thing):
        pass

    __axioms__ = [ EquivalentClasses(MenuItem, ObjectUnionOf(Food, Beverage)) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class MenuItem(Thing):
        equivalent_to = ObjectUnionOf(Food, Beverage)
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- EquivalentClasses
    EquivalentClasses --> "*" ClassExpression : operands
    ```
    """

    operands: Tuple[ClassExpression, ...] = field(default_factory=tuple)

    def __init__(self, *operands: ClassExpression):
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        num_ops = len(self.operands)
        sentences: List[Sentence] = []
        for i in range(num_ops - 1):
            for j in range(i + 1, num_ops):
                sentences.append(Iff(instance_of(I, self.operands[i]), instance_of(I, self.operands[j])))
        return Forall([I], _conjunction(sentences))

@dataclass
class EquivalentObjectProperties(Axiom):
    """
    An equivalent-object-properties axiom.

    Example of explicit declaration:

    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    class HasChild(TopObjectProperty):
        '''A property that relates a person to their child'''
        domain = Person
        range = Person

    __axioms__ = [ EquivalentObjectProperties(HasParent, ObjectInverseOf(HasChild)) ]
    ```

    Normally, the more Frame-style equivalent is preferred:

    ```python
    class HasChild(TopObjectProperty):
        equivalent_to = ObjectInverseOf(HasParent)
    ```

    In this particular case, a simpler more conventional way to declare the inverse is:

    ```python
    class HasChild(TopObjectProperty):
        range = Person
        domain = Person
        inverse_of = HasParent
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- EquivalentObjectProperties
    EquivalentObjectProperties --> "*" ObjectPropertyExpression : operands
    ```

    """

    operands: Tuple[ObjectPropertyExpression, ...] = field(default_factory=tuple)

    def __init__(self, *operands: ObjectPropertyExpression):
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        num_ops = len(self.operands)
        sentences: List[Sentence] = []
        for i in range(num_ops - 1):
            for j in range(i + 1, num_ops):
                sentences.append(Iff(instance_of_op(I, J, self.operands[i]), instance_of_op(I, J, self.operands[j])))
        return Forall([I, J], _conjunction(sentences))

@dataclass
class EquivalentDataProperties(Axiom):
    """
    An equivalent-data-properties axiom.

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- EquivalentDataProperties
    EquivalentDataProperties --> "*" DataPropertyExpression : operands
    ```
    """

    operands: Tuple[DataPropertyExpression, ...] = field(default_factory=tuple)

    def __init__(self, *operands: DataPropertyExpression):
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        num_ops = len(self.operands)
        sentences: List[Sentence] = []
        for i in range(num_ops - 1):
            for j in range(i + 1, num_ops):
                sentences.append(Iff(instance_of_dp(I, J, self.operands[i]), instance_of_dp(I, J, self.operands[j])))
        return Forall([I, J], _conjunction(sentences))

@dataclass
class DisjointObjectProperties(Axiom):
    """
    A disjoint-object-properties axiom.

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- DisjointObjectProperties
    DisjointObjectProperties --> "*" ObjectPropertyExpression : operands
    ```
    """

    operands: Tuple[ObjectPropertyExpression, ...] = field(default_factory=tuple)

    def __init__(self, *operands: ObjectPropertyExpression):
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        num_ops = len(self.operands)
        sentences: List[Sentence] = []
        for i in range(num_ops - 1):
            for j in range(i + 1, num_ops):
                sentences.append(
                    Not(And(instance_of_op(I, J, self.operands[i]), instance_of_op(I, J, self.operands[j])))
                )
        return Not(Exists([I, J], Or(*sentences)))

@dataclass
class DisjointDataProperties(Axiom):
    """
    A disjoint-data-properties axiom.

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- DisjointDataProperties
    DisjointDataProperties --> "*" DataPropertyExpression : operands
    ```
    """

    operands: Tuple[DataPropertyExpression, ...] = field(default_factory=tuple)

    def __init__(self, *operands: DataPropertyExpression):
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        num_ops = len(self.operands)
        sentences: List[Sentence] = []
        for i in range(num_ops - 1):
            for j in range(i + 1, num_ops):
                sentences.append(
                    Not(And(instance_of_dp(I, J, self.operands[i]), instance_of_dp(I, J, self.operands[j])))
                )
        return Not(Exists([I, J], Or(*sentences)))

@dataclass
class DisjointClasses(Axiom):
    """
    A disjoint-classes axiom.

    Example of explicit declaration:

    ```python
    class Food(Thing):
        pass

    class Beverage(Thing):
        pass

    __axioms__ = [ DisjointClasses(Food, Beverage) ]
    ```

    Sometimes, the more Frame-style equivalent is preferred:

    ```python
    class Food(Thing):
        pass

    class Beverage(Thing):
        disjoint_with = Food
    ```

    However, the choice of which element of the tuple is the first class is arbitrary,
    so declaration of a top level axiom may be simpler (especially when more than
    two classes are members, or class expressions are involved).

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- DisjointClasses
    DisjointClasses --> "*" ClassExpression : operands
    ```
    """

    operands: Tuple[ClassExpression, ...] = field(default_factory=tuple)

    def __init__(self, *operands: ClassExpression):
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        num_ops = len(self.operands)
        sentences: List[Sentence] = []
        for i in range(num_ops - 1):
            for j in range(i + 1, num_ops):
                sentences.append(Not(And(instance_of(I, self.operands[i]), instance_of(I, self.operands[j]))))
        return Not(Exists([I], Or(*sentences)))

@dataclass
class DisjointUnion(Axiom):
    """
    A disjoint-union axiom.

    Example of explicit declaration:

    ```python
    class Food(Thing):
        pass

    class Beverage(Thing):
        pass

    class MenuItem(Thing):
        pass

    __axioms__ = [ DisjointUnion(MenuItem, Food, Beverage) ]
    ```

    Sometimes, the more Frame-style equivalent is preferred:

    ```python
    class Food(Thing):
        pass

    class Beverage(Thing):
        disjoint_union_of = MenuItem
    ```

    UML:

    ```mermaid
    classDiagram
    Axiom <|-- DisjointUnion
    DisjointUnion --> "1" ClassExpression : first
    DisjointUnion --> "*" ClassExpression : operands
    ```
    """

    first: Class
    operands: Tuple[ClassExpression, ...] = field(default_factory=tuple)

    def __init__(self, first: Class, *operands: ClassExpression):
        self.first = first
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        eq = Forall([I], Iff(instance_of(I, self.first), Or(*[instance_of(I, op) for op in self.operands])))
        num_ops = len(self.operands)
        disj: List[Sentence] = []
        for i in range(num_ops - 1):
            for j in range(i + 1, num_ops):
                disj.append(Not(And(instance_of(I, self.operands[i]), instance_of(I, self.operands[j]))))
        return And(eq, Not(Exists([I], Or(*disj))))

@dataclass
class AnonymousClassExpression(ABC):
    """
    An base class for anonymous class expressions.
    """

    def as_fol(self) -> Optional[Sentence]:
        raise NotImplementedError(f"{self} Must implement as_fol method")

@dataclass
class InverseObjectProperty:
    """
    An inverse object property expression.

    Example:
    -------
    ```python
    class HasParent(TopObjectProperty):
        '''A property that relates a person to their parent'''
        domain = Person
        range = Person

    class HasChild(TopObjectProperty):
        '''A property that relates a person to their child'''

    __axioms__ = [ EquivalentObjectProperties(HasParent, InverseObjectProperty(HasChild)) ]
    ```

    UML:

    ```mermaid
    classDiagram
    InverseObjectProperty --> "1" ObjectPropertyExpression : property
    ```

    """

    first: ObjectProperty

    def as_fol(self) -> Optional[Sentence]:
        raise AssertionError("Not to be called directly")

@dataclass
class ObjectIntersectionOf(AnonymousClassExpression):
    """
    A ClassExpression that is the intersection of a list of ClassExpressions.

    Example of explicit axiom declaration:

    ```python
    class Pizza(Thing):
        pass

    class Cheesy(Thing):
        pass

    class CheesyPizza(Thing):
        pass

    __axioms__ = [ EquivalentClasses(CheesyPizza, ObjectIntersectionOf(Pizza, Cheesy)) ]
    ```

    It is more idiomatic to declare axioms implicitly in Frame-style class definitions:

    ```python
    class CheesyPizza(Thing):
        equivalent_to = ObjectIntersectionOf(Pizza, Cheesy)
    ```

    UML:

    ```mermaid
    classDiagram
    AnonymousClassExpression <|-- ObjectIntersectionOf
    ObjectIntersectionOf --> "*" ClassExpression : operands
    ```

    """

    operands: Tuple[ClassExpression, ...] = field(default_factory=tuple)

    def __init__(self, *operands: ClassExpression):
        self.operands = operands

    def as_fol(self) -> Sentence:
        return And(*[instance_of(I, op) for op in self.operands])

@dataclass
class ObjectUnionOf(AnonymousClassExpression):
    """
    A ClassExpression that is the union of a list of ClassExpressions.

    Example of explicit axiom declaration:

    ```python
    class Pizza(Thing):
        pass

    class CheeseOnToast(Thing):
        pass

    class Pizzaesque(Thing)
        pass

    __axioms__ = [ EquivalentClasses(Pizzaesque, ObjectUnionOf(Pizza, CheeseOnToast)) ]
    ```

    It is more idiomatic to declare axioms implicitly in Frame-style class definitions

    ```python
    class Pizzaesque(Thing):
        equivalent_to = ObjectUnionOf(Pizza, CheeseOnToast)
    ```

    UML:

    ```mermaid
    classDiagram
    AnonymousClassExpression <|-- ObjectUnionOf
    ObjectUnionOf --> "*" ClassExpression : operands
    ```
    """

    operands: Tuple[ClassExpression, ...] = field(default_factory=tuple)

    def __init__(self, *operands: ClassExpression):
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        return Or(*[instance_of(I, op) for op in self.operands])

@dataclass
class ObjectComplementOf(AnonymousClassExpression):
    """
    A ClassExpression that is the complement of a ClassExpression.

    Example of explicit axiom declaration:

    ```python
    class Pizza(Thing):
        pass

    class MeatPizza(Thing):
        pass

    class VegetarianPizza(Thing):
        pass

    __axioms__ = [ EquivalentClasses(VegetarianPizza, ObjectIntersectionOf(Pizza, ObjectComplementOf(MeatPizza))) ]
    ```

    It is more idiomatic to declare axioms implicitly in Frame-style class definitions

    ```python
    class VegetarianPizza(Thing):
        equivalent_to = ObjectIntersectionOf(Pizza, ObjectComplementOf(MeatPizza))
    ```

    UML:

    ```mermaid
    classDiagram
    AnonymousClassExpression <|-- ObjectComplementOf
    ObjectComplementOf --> "1" ClassExpression : first
    ```
    """

    first: ClassExpression

    def as_fol(self) -> Optional[Sentence]:
        return Not(instance_of(I, self.first))

@dataclass
class ObjectOneOf(AnonymousClassExpression):
    """
    A ClassExpression that is the set of individuals.

    Example of explicit axiom declaration:

    ```python
    class Unit(Thing):
        pass

    inch = Unit("inch")
    cm = Unit("cm")
    m = Unit("m")

    class LengthUnit(Unit):
        pass

    __axioms__ = [ EquivalentClasses(LengthUnit, ObjectOneOf(inch, cm, m)) ]
    ```

    It is more idiomatic to declare axioms implicitly in Frame-style class definitions

    ```python
    class LengthUnit(Unit):
        equivalent_to = ObjectOneOf(inch, cm, m)
    ```

    UML:

    ```mermaid
    classDiagram
    AnonymousClassExpression <|-- ObjectOneOf
    ObjectOneOf --> "*" Individual : operands
    ```
    """

    operands: Tuple[Individual, ...] = field(default_factory=tuple)

    def __init__(self, *operands: Individual):
        self.operands = operands

    def as_fol(self) -> Optional[Sentence]:
        return Or(*[Term("eq", I, individual_name(ind)) for ind in self.operands])