Logic as a Tool

Chapter 5Applications: Mathematical Proofs and Automated Reasoning

Logical systems are used in practice to perform formal reasoning that goes beyond pure logic. Most often they are used for mathematical reasoning, but they have also found numerous other applications in artificial intelligence, especially the field of knowledge representation and reasoning (e.g. various description logics for ontologies), as well as in many areas of computer science including database theory, program analysis, and deductive verification. In each of these areas the use of deductive systems is guided by the specific applications in mind, but the underlying methodology is the same: the purely logical engine of the deductive system, which consists of the general, logical axioms and inference rules is extended with specific, non-logical axioms and rules describing the particular subject area. The logical and non-logical axioms and rules together constitute a formal theory in which the formal reasoning is performed by means of derivations from a set of assumptions in the chosen deductive system. These assumptions are usually the relevant non-logical axioms, plus other specific ad hoc assumptions applying to the concrete domain or situation for which the reasoning is conducted.

Most typical mathematical theories describe classes of important relational structures such as sets, partial or linear orders, directed graphs, trees, equivalence relations, various geometric structures, etc., algebraic structures ...