The field of formal semantics is the study of the interpretations of formal languages. A language wether it is natural or formal can be defined without explicitly giving any meaning to its sentences or expressions. Basically, an interpretation of a formal language is a mapping that provides a meaning to each elementary symbols and a set of rules to decide if a statement made in this language is true or false.
Unlike in natural languages, ambiguities can not be tolerated in reasoning or mathematical languages. When the meaning of symbols is subjective, two different individuals may have a different interpretation of the symbols and inferences made. To avoid this problem, the semantics of these symbols is established according to a common consensus and written in a formal language : the formal semantics. Formal semantics are usually expressed in a mathematical language (for example, set theory) or logic (for example, first-order logic). These languages are undoubtedly the best candidates for its definition because they hold a strong power of expression, allow to establish rigorous demonstrations and have been used and studied for several centuries by the scientific community. The existence of a formal semantics for a language does not call into question the utility of the latter: indeed, one might ask if it is not ultimately simpler to use formal semantics directly (which is itself a language properly speaking) to represent knowledge and to abandon the language to which this formal semantics has been associated.
In general, the language chosen to define formal semantics often provides high or even unlimited expressivity. Computability problems increase with the expressiveness of language. For example, the problem of determining whether between two formulas of first-order logic one is deduced from the other is semi-decidable; this means that, depending on the case, one can not decide whether or not one of the formulas is deduced from the other. Nevertheless, when considering some less expressive fragments of first-order logic, the problem of semidecidability no longer arises (for example, the conjunctive positive existential fragment of predicate logic or the guarded fragment). When one of these decidable fragments is chosen to constitute the formal semantics of a KRR language, the latter inherits its power of expression and its computational characteristics but is also required to offer a syntax and its own operations; and that’s where his main interest lies. In case of doubt about the meaning of an expression established in the syntax, formal semantics is authoritative to eliminate ambiguity or contradiction.
Concerning operations directly defined in a KRR language, it is an interesting option when it is inspired by a mathematical theory different from that of which its formal semantics is derived (for example, graph theory). Such a choice may be wise if it is easier to define efficient algorithms in this theory, for example. One can then check if the result obtained by applying the operation on the expressions of the KRR language is coherent by comparing it with that defined by the formal semantics of the said operation. From a practical point of view, formal semantics is mainly used by specialists of Knowledge Base Systems (KBS) to ensure that the KBS is behaving as expected by comparing the meaning of the reasoning operations performed and the KRR languages used. It aims at determining if the reasonings realized by a KBS are correct and complete compared to the formal semantics of the language used. Informally, a reasoning is said to be correct when it has not led to the deduction of more knowledge than expected in the formal semantics. Complementarily, reasoning is said to be complete when none of the deductions provided by the formal semantics are missing. These checks and comparisons make it possible to ensure that two different KBS designed for the same purpose do not lead to a representation or production of knowledge with divergent meaning.