The formal specification of legal ontology