A good reading from WikiBooks

Artical from: http://en.wikibooks.org/wiki/Logic_for_Computer_Scientists/Introduction

Please try not to repost this article somewhere else! thanks --gcseed

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.