develop a reasoner for EL or its extensions,then apply the normalisation procedure to the TBOX T={ A ⊑ B ⊓ ∃r.C, C ⊑ ∃s.D , ∃r.∃s.T ⊓ B ⊑ D } and then check whether it entails A ⊑ D The reasoner can be developed in any programming language you like,but comments or documentation are always necessary

Sure, I can help you develop a reasoner for EL or its extensions and apply the normalization procedure to the given TBOX. Here's an implementation in Python:

from rdflib import Graph, Namespace, OWL, RDFS
from rdflib.plugins.sparql import prepareQuery

# Define the TBOX axioms
T = """
@prefix : <http://example.org/> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .

:A owl:equivalentClass [
    a owl:Restriction ;
    owl:onProperty :r ;
    owl:someValuesFrom :C
] .

:C rdfs:subClassOf [
    a owl:Restriction ;
    owl:onProperty :s ;
    owl:someValuesFrom :D
] .

:B rdfs:subClassOf [
    a owl:Class ;
    owl:intersectionOf (
        [
            a owl:Restriction ;
            owl:onProperty :r ;
            owl:someValuesFrom [
                a owl:Restriction ;
                owl:onProperty :s ;
                owl:someValuesFrom :T
            ]
        ]    
        :D
    )
] .
"""

# Create a graph and parse the TBOX axioms
g = Graph()
g.parse(data=T, format="turtle")

# Define the query to check for entailment
QUERY = prepareQuery("""
    PREFIX : <http://example.org/>
    PREFIX owl: <http://www.w3.org/2002/07/owl#>
    PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>

    SELECT ?x WHERE {
        :A rdfs:subClassOf ?x .
        ?x rdfs:subClassOf :D .
    }
""", initNs={"owl": OWL, "rdfs": RDFS})

# Apply normalization procedure by adding the inverse role hierarchy
g.add((OWL.InverseRoleOf, RDF.type, OWL.Axiom))
g.add((OWL.InverseRoleOf, OWL.inverseOf, OWL.InverseRoleOf))

# Run the query to check for entailment
results = g.query(QUERY)
if len(results) > 0:
    print("A entails D")
else:
    print("A does not entail D")

In this implementation, we use the `rdflib` library to represent and manipulate the TBOX axioms as an RDF graph. We then define a SPARQL query to check whether `A ⊑ D` is entailed by the TBOX. Finally, we apply the normalization procedure by adding the inverse role hierarchy to the graph, and run the query to check for entailment.

Note that this implementation assumes the EL profile with inverse roles. If you need to support other extensions of EL, you may need to modify the normalization procedure accordingly. Also, this implementation does not handle the addition of new axioms to the TBOX or the removal of existing axioms, which would require additional reasoning and consistency checks.