Ontologies on the Semantic Web often implement mathematical logic, a subfield of Mathematics dealing with formal expressions, deductive reasoning, and formal proof. Description Logic (DL) is a family of formal knowledge representation languages in Artificial Intelligence used for logical formalism for ontologies, including formal reasoning of the concepts of a knowledge domain. Description Logic languages are more expressive than propositional logic (which deals with declarative propositions and does not use quantifiers), and more efficient in decision problems than first-order predicate logic (which uses predicates and quantified variables over non-logical objects). A Description Logic can model concepts, roles and individuals, and their relationships. A core modeling concept of a Description Logic is the axiom, which is a logical statement about the relation between roles and/or concepts. Most web ontologies written in OWL are implementations of a Description Logic.
Each Description Logic Knowledge Base (KB) consists of a terminological part (TBox) and an assertional part (ABox), both of which contain a set of axioms. A basic Description Logic is AL, the Attributive Language, which supports atomic negation, concept intersection, universal restrictions, and limited existential quantification.