Logic for Computer Scientists/Introduction

Introduction Although logic was developed and researched since Aristotle and Megara (430 - 360 b.c.) we want to focus to the development of mathematical logic, for which Gottfried Frege can be seen as the founder (Begriffsschrift, 1879). That was the first time, logic was introduced in a totally formal language; of course there have been others like Leibniz and Boole who contributed to the formalisation of logic, but it was Frege who radically introduced the idea of formalisation and deduction. This aspect is of particular interest for computer science, because there, the automation of the deduction process is investigated. The development of modern mathematical logic came along with a deep crisis in mathematics: At the end of the 19th and the beginning of the 20th century axiomatisation of set theory and of arithmetic have been a focus of mathematical research and in 1910 -1913 Whitehead and Rusell published their Principia Mathematica, an attempt to formalise the entire mathematics on the grounds of a formal logic, which was essentially the one given by Frege. This formalisation made it possible to avoid a number of antinomies, which have been discussed at that time. However it was in 1931, that Kurt Goedel proved in his famous incompleteness theorems, that an approach to formalise arithmetic cannot be complete given its consistency. It is important to note that during this period in the 1930th the foundation of theoretical computer science was laid: Alan Turing published his work on theoretical machines and on computability, Alonso Church developed his -calculus and Stephen Kleene developed the foundations of recursion theory. For the rest of this introduction we will directly jump into the use of logic for modern computer science. The reader who is interested in history of logic is referred to the bibliographic section at the end of this introduction. Programming Within the last decade it turned out that computerised systems are the very base of advanced technology. Software is present in nearly all devices of modern houses, in our cars, not to speak about aircrafts or weapons. Without going into details, it is immediately obvious that for most, if not all applications, robust, safe and correct behaviour of a system is mandatory. To achieve this it is widely accepted that it is only possible if formal methods are applied during the entire process of hard- and software-development. In the following we shortly depict some tasks where the use of logic has proved to be extremely helpful. Abstract Datatypes In order to define datatypes and to derive efficient implementations for it, the concept of abstract datatype definitions is central. The idea is to define the abstract properties of a datatype, instead of giving special realisations. A very trivial example is the definition of a stack: Let be an alphabet. In order to define a stack over we assume to be a nullary function and we define the following properties of stacks: Hence, we have the functions and , which yield stacks and the predicate , furthermore we need the following properties with respect to the -operation. And we have to give properties with respect of the combinations of functions: The above formulae state what properties we expect stacks to have. Obviously it contains no hints how to implement such a data type. And indeed this specification is aiming to solve other problems, e.g. Is the specification correct? I.e. is there a set together with the given operations, such that the axioms above hold? Is the specification complete. I.e. do the axioms imply all the properties we intuitively assume a stack to have? Are there sets which do not meet our expectations? The reader may have already noticed, that the axioms are nothing else than formulas in predicate logic, i.e. all logic where variables like or together with so called quantifiers and are used. The above two questions, namely correctness and completeness, are very central topics for the design of formal systems in logic. The proof of these properties often is difficult and costly, but on the other hand it is one of the clear advantages of logical systems, that these properties can be proved formally. In the main part of this course we will deal with these questions explicitly. Program Developments There are a number of attempts to define methods, which allow the development of a program together with a formal argument of its correctness. We will give a very rough idea with a toy example. Assume the following simple program contains a loop, and assume that it has an array of integers: max := a(1); do i = 2,n if a(i) > max then max := a(i) end In order to understand what is going on if this program is executed, the following so called loop invariant is helpful: This means, that for every value of , i.e. before and after every execution of the if-statement within the do-loop the above formula is valid. Now assume that the loop is executed the last time, hence the value of after executing of the loop-body is , one can conclude that max contains the maximum value of the array: Another important issue for program development is the specification of programs. In order to give a formal specification of the above program for finding the maximum of an array the following logical formula can be used: Note that in this specification is assumed to be a set. There is no decision yet made, that this has to be implemented by means of an array. On the other hand logic can be used not only for the specification but also as programs itself. The following is a logic program which computes the maximum value of a list of values. Lists are represented as [ head.tail ], where head denotes the front element of a list, tail the rest of the list and nil the empty list. max([m.nil], m) <- . max([head.tail], m) <- max([tail], m), head < m. max([head.tail], head) <- max([tail], m), head >= m. Artificial Intelligence One of the oldest sub-disciplines of Artificial Intelligence (AI) research is automated theorem proving. In the early days some were very optimistic about using theorem provers as general problem solvers for various different tasks, like action planning, knowledge representation or program verification. Now it is clear, that for special tasks tailored reasoning systems are necessary. We will comment in this subsection on theorem proving, aiming at proving mathematical theorems and on knowledge representation. This idea can be seen as going back to the ideas of Gottfried Wilhelm Leibnitz (1646 - 1716), who already at this time had a dream of formalisation, and even automatisation of mathematics. A recent success is the proof of Robbins conjecture, which even reached the New York Times. For details see http://www-unix.mcs.anl.gov/~mccune/papers/robbins/. In 1933, E. V. Huntington presented the following basis for Boolean algebra: x + y = y + x. [commutativity] (x + y) + z = x + (y + z). [associativity] n(n(x) + y) + n(n(x) + n(y)) = x. [Huntington equation] Shortly thereafter, Herbert Robbins conjectured that the Huntington equation can be replaced with a simpler one: n(n(x + y) + n(x + n(y))) = x. [Robbins equation] Robbins and Huntington could not find a proof, and the problem was later studied by Tarski and his students. The proof that solves the Robbins problem was found October 10, 1996, by the theorem prover EQP. EQP is similar in many ways to the more well known program http://www.mcs.anl.gov/AR/otter/. The main differences are that EQP has associative-commutative (AC) unification, is restricted to equational logic, and offers more paramodulation strategies. See the http://www.mcs.anl.gov/~mccune/papers/33-basic-test-problems/ for details. Knowledge Representation In many Artificial Intelligence the representation and manipulation of knowledge is a central task. To this end numerous graphic-oriented formalisms have been invented. An informal semantics of this graphical notation states, that both, man and animal are mammal and that man have a nationality and an age, whereas an animal has age and no nationality. A closer investigation of the semantics of such a formalism would show, that this is nothing than a pictorial representation of the following set of predicate logic formulae: See also: Gellrich/Gellrich: Mathematik (1) - Schaltalgebra Example: File:Knowledge Representation.png Problems Problem 1 (Introduction) In a criminal case the following facts are proved: At least one of the three persons X,Y,Z is guilty. If X is guilty and Y is innocent, then Z is guilty. These circumstances are not sufficient to accuse one of them but it can be said for certain that at least one of two persons must be guilty. Which two are these? Problem 2 (Introduction) Which of the following syllogisms are valid? Give a reason for your answer or give a counterexample. All are , some are not then: Some are . All are , some are not then: Some are not All are , some are not then: Some are not . Problem 3 (Introduction) In a meeting there are 100 politicians discussing with each other. Everyone of them is either corrupted or uncorrupted. The Following facts are known: at least one politician is uncorrupted. In each pair of two politicians is at least one corrupted . How Many of the politicians are corrupt, how many are uncorrupted? Problem 4 (Introduction) The anthropologist Abercrombie entered the island of the knights and the mucker with a slack feeling he have never had before. He knew that very wondrous people lived on this island: The knights made only true propositions the mucker false propositions every time. Abercrombie knew also that he had to find a friend before he could experience something. He had to find someone whose propositions he can trust. So he asked the first three people of the island he met to find a knight. Abercrombie asked Arthur at first: Are Bernard and Charles both knights? Arthur answered: Yes they are! Abercrombie asked then: Is Bernard a knight? With a big surprise he get the answer: No! Is Charles a knight or a mucker? Deduce your answer and give a reason for it. Problem 5 (Introduction) A little island had exactly 100 inhabitants. Every inhabitant either always told the truth or always lied. One Researcher came one day on the island and questioned the inhabitants sequentially. The first told: "There is at least one liar with us." The second said: "At least two liars live among us." etc.. The last finally claimed: "There are 100 liars on this Island." How many liars were there really? The researcher went to another island with 99 Inhabitants a year later. In an interview the inhabitants of these island spoke completely corresponding like on the first island, i.e. the th inhabitants said: "There are at least liars here." What can you say about this island? Problem 6 (Introduction) In a village the priest explained one Sunday: "It was confessed to me that there are men who are unfaithful in our village. However, the confessing secret forbids it to me to call the names. It will you nevertheless learn all of them, if we proceed as follows: Any woman who for certain knows that her husband is unfaithful shall throw him in the following night out of the house." However, the problem was that every woman knows all about every other husband but nothing about her husband. In the next morning the priest went through the streets; not one single man was turned adrift. Also on the next day he saw nobody. But at 100th acre he saw men, who had been thrown out of the house by their wifes. How many? Problem 7 (Introduction) There is a hotel with countable infinitely many rooms 0, 1, 2,.... All rooms are vacant. Now, a -decker bus comes with many seats on every deck. How can all of the passengers be accommodated in the hotel? Up to Logic for Computer Scientists