Construction of Proofs

Abstract

The primary means of reasoning in a logic are calculi, collections of purely syntactic operations that allow us to determine whether a given formula is valid. Two such calculi are defined in Chap. 2 and 3 for first-order predicate logic and for dynamic logic (DL). Having such calculi at hand enables us in principle to create proofs of arbitrarily complex conjectures, using pen and paper, but it is obvious that we need computer support for all realistic applications. Such a mechanised proof assistant primarily helps us in two respects: 1. The assistant ensures that rules are applied correctly, e.g., that rules can only be applied if their side-conditions are not violated, and 2. the assistant can provide guidance for selecting the right rules. Whereas the first point is a necessity for making calculi and proofs meaningful, the second item covers a whole spectrum from simple analyses to determine which rules are applicable in a certain situation to the complete automation that is possible for many first-order problems.