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 ...*

Start Free Trial

No credit card required