Is calculus important for computer science required

Logical Calculi in Computer Science

1. Introduction

What does science mean? The interplay between theory and experiment is essential. As part of a theory, the facts of the everyday world are modeled abstractly, mostly in the language of mathematics. There, conclusions are drawn with mathematical precision from the abstraction of known facts. These in turn have to be checked against reality, i.e. through an experiment. So it's about things like:
  • Explainability of observed phenomena in the real world by conclusions from mathematics,
  • Predictability of real world phenomena through logical inferences from mathematics.
Language is also an important part of the real world. What has just been said can therefore also be applied to language. Logic can be viewed as the corresponding mathematical abstraction from parts of language. As with every language, the syntax of the abstract language of logic, i.e. its formal structure, its “sentence structure”, and its semantics, i.e. the meaning of the individual possible language fragments, must be examined. Different examined language fragments lead to different logics.
In this book, therefore, very different logics are considered, including:

    2. propositional logic

    Propositional logic is the simplest form of logic. It describes the simplest links between elementary statements that are regarded as atomic (“indivisible”). The practical importance of the AL in computer science cannot be overestimated. Boolean expressions occur in every programming language and they are also indispensable in circuit design. In the AL, artificial, abstract situations can be analyzed with mathematical precision. The syntactic question of whether a formula is well-formed is offset by the semantic question of the validity of a formula.
    If the validity of a formula F is to be clarified, a truth table can be used. It's a purely semantic approach. An alternative and usually faster approach could be as follows: Re-form F syntactically through predetermined conclusions until you get the desired conclusion. During the transformations, attention is only paid to the shape of the formulas. A finite set of such transformation rules, a kind of “toolbox”, is used. Such a “toolbox” is called a calculus. In general, some requirements are placed on a calculus. Correctness means that everything that can be deduced in the calculus is true. Completeness means that every true formula can be derived in the calculus. The general goal of a calculus, therefore, is to be complete and correct. Different calculi for propositional logic are presented.

    3. Predicate logic

    The most obvious syntactic difference between the AL and the PL, the two most important logical formalisms in computer science (and beyond), is the existence of two additional symbols, the universal quantifier (") and the existential quantifier ($), which refer to additional language fragments Closely related to this is the difference that nothing is stipulated in the AL about the statements. These are represented there by variables, but the only thing you want to express about statements is whether they are true or false.
    In the PL, on the other hand, a more detailed analysis of the statements is carried out. In particular, it is shown who is said about what. A very noticeable difference is therefore that there are formulas in the PL, that is, statements that can be true or false, as well as terms; these are expressions that refer to individuals.
    Some issues related to calculi in the PL are addressed:
    • Kurt Gödel's predicate calculus.
    • Syllogisms are presented as an (incomplete) calculus of the PL. Their treatment is illustrated by Lewis Carroll's "Game of Logic".
    • There is an introduction to the SLD calculation.

    4. The SLD calculus (logic programming)

    The best-known programming language that uses logic operationally to answer given questions directly through logical inferences is Prolog. Prolog can be roughly divided into two parts: the logical and the non-logical components. The purely logical parts of “Prolog”, the “logic programming”, consider special predicate logic formulas, the so-called “Horn clauses”. These can be handled quite intuitively by a calculus with a single rule, the SLD rule. The meaning of logic programs is given by two semantics: the operational and the denotational.
    These two semantics are equivalent, which ultimately means that the SLD calculus is complete and correct.

    5. Hoare's logic

    One of the most important tasks of information processing with a computer is to create correct programs. The term “correct program” alone is still too vague. What does it mean that a program is "correct"? A correct program must meet a requirement or specification. So in order to be able to talk about correct programs at all, you need three things:
    • a programming language, the elements of which are the correctly formed programs,
    • a specification language, the elements of which are the correctly formed specifications,
    • a correctness concept that decides whether a given program meets a given specification.
    In this generality, the problem is unfortunately undecidable. This is a consequence of Rice's theorem about Turing machines. In the HL, the calculus-based verification of programs is carried out by Hoaresche Tripel. These are triples {F} S {G} for which the following applies:
    • S is a simple program
    • F, G are formulas of the PL that describe the input and the resulting output.
    Calculi for Hoaresche triples with a small program scope are presented.

    6. Modal logic

    The primary goal of modal logic is the recording and formal treatment of language fragments such as “necessarily”, “possibly”, “accidentally”. Such are mentioned in the context of the ML modalities. Through these fragments, modal logic can express many everyday things very elegantly, mathematically precisely and close to normal colloquial language. The ML can also serve as a mathematical underpinning for other logics presented in the following chapters.
    On the syntactic level, some classic calculi and then the associated semantic formalisms, the Kripke semantics, are presented.
    An outstanding result is the equivalence theorem, which states that the most widespread calculi in practice can also be semantically characterized by very fundamental relational properties.
    Intuitionistic logic proves to be a special logic that can be easily explained with the help of ML. It's a form of logic that has a constructive approach behind it. A statement is only considered certain if it is not only confirmed by an indirect proof but is actually given by an explicit proof. For example, the excluded third party sentence does not apply in the IL.

    7. Temporal logic

    The TL is indispensable for the formal verification of real-time systems. The modal concept of necessity can be interpreted temporally as “always”. It is about logical relationships between actions, which mostly amount to a special form of temporal quantification. The TL is more flexible than a pure presentation of facts by the PL.
    In this chapter several calculi are presented, from the classic simple Minimal Tense Logic to the modern, very elegant and meaningful Duration Calculus.
    At the level of the Kripke semantics for a modal temporal logic, the time domains can be adapted very well to practical needs:
    • as an equivalence relation or with weaker relational properties,
    • as total order or as branching time, as appropriate in parallel systems,
    • with discrete or continuous time,
    • with time that can be measured, i.e. with precisely measurable time information.

    8. Epistemic Logic

    In EL, the terms “knowledge” and “belief” of statements are formalized with the help of suitable modalities. The resulting calculi are very similar to the classic calculi of ML. The semantic treatment by Kripke structures can also be transferred very well from the ML to the EL, with the necessity modality being replaced by an operator that expresses knowledge; and as in ML, the equivalence theorem and other powerful equivalence theorems can then be proven.
    The EL can be used in computer science, for example, for the formal description of multi-agent systems. Then there is not just one modal operator as in ML, but one for each agent. This allows the concepts of shared and shared knowledge to be precisely mathematized. The treatment can be largely based on the methods of ML.

    9. Deontic logic

    The DL is dedicated to researching moral norms, not just in the form of individual rules, but as a whole system. It is about expressions of the form “something is compulsory”, “something is allowed” or “something is forbidden”. The necessity of moral restrictions in computer science and science in general is evident.
    Their formal treatment within the framework of a purely calculative DL, however, encounters great difficulties. In the previous formal systems, such as the system called "Old System (OS)", where formal modal logic was made the basis of the DL for the first time, and the later "Standard System of Deontic Logic (SDL)", serious deficiencies and absurd consequences were found which show how difficult it is to treat norms in a consistent manner.
    A possible but very abstract way out is not to formulate deontic sentences as generally valid but only to formulate them in relation to a non-empty set of norms. Such sets of standards are called “codes”.

    10. Non-monotonous logic

    Non-monotonic logic (NML) is about a phenomenon that occurs frequently in artificial intelligence: a lot of facts have already been secured. Now new knowledge is added. However, this does not increase the amount of known knowledge, but rather some of the apparently well-known facts become invalid. A prime example of this is “Tweety, the AI ​​bird”: If only Tweety is known that he is a bird, the fact that birds can generally fly leads to the conclusion that Tweety can fly. If, on the other hand, Tweety is examined more closely and identified as a penguin who can then not fly, the conclusion on Tweety's ability to fly must be revised. One would like to be able to treat this phenomenon formally exactly.
    In the truth maintenance systems presented, a distinction is made between secure and insecure knowledge. A valid model for a set of (partly uncertain) justifications may only contain well-founded knowledge through inferences and must include all consequences of valid justifications. Such models do not necessarily have to exist, and they are usually ambiguous.
    The JTMS algorithm presented here shows how a model that is also permissible for the new situation can be constructed from a permissible model when new facts are obtained, if one exists.

    11. Default logics

    While in truth maintenance systems the non-monotonic derivation is in the foreground and non-monotonic rules are used more as a means to an end, the insecure rules, default rules or simply called defaults, represent the backbone of what is happening in the default logic are characterized by the fact that they allow exceptions and therefore do not apply in general but only typically. They are valid as long as the opposite has not been explicitly proven.
    It is about a (possibly infinite) procedure for the accumulation of consequences, always alternating by means of classical deduction and by means of defaults. The search is reduced to a fixed point problem, and much of what is known from various fixed point theories can be used. A possibly finite method for determining the consequences can be provided by the creation of process trees.

    12. Mathematical basics

    This chapter compiles some math tools that will help you understand the previous chapters. Here, too, complex accumulations of terms are dispensed with and the material is only offered as far as it is actually needed.

    Backmatter