South African Computer Journal 1993(9) http://hdl.handle.net/10500/23882 2020-09-29T03:57:44Z 2020-09-29T03:57:44Z Introduction to computability theory Zucker, J Pretorius, L http://hdl.handle.net/10500/24126 2018-05-29T01:00:52Z 1993-01-01T00:00:00Z Introduction to computability theory Zucker, J; Pretorius, L These are notes for a short introductory course on Computability Theory (or recursive function theory). The basic notion of computability is defined in terms of a simple imperative programming language. 1993-01-01T00:00:00Z A working relational model: The derivation of the Dijkstra-Scholten predicate transformer semantics from Tarski's axioms for the Peirce-Schroder calculus of relations Maddux, RD http://hdl.handle.net/10500/24125 2018-05-29T01:00:53Z 1993-01-01T00:00:00Z A working relational model: The derivation of the Dijkstra-Scholten predicate transformer semantics from Tarski's axioms for the Peirce-Schroder calculus of relations Maddux, RD The definitions for Dijkstra's predicate transformer semantics can be justified by considering the meaning of a program as a binary relation on states (which holds between two states if there is a terminating computation connecting them) together with a set of states (those which initiate eternal computations). In fact, all of the definitions can be proved as theorems, using Tarski's ten equational postulates for the calculus of relations. These postulates define relation algebras, so we take the meaning of a program to be a pair of elements of a complete relation algebra, one corresponding to the binary relation determined by the terminating computations, the other corresponding to the set of states initiating eternal computations. The predicate transformers for a program are defined from these two elements. In this abstract setting we derive all the significant definitions and theorems of Dijkstra and Scholten's "Predicate Calculus and Program Semantics''. 1993-01-01T00:00:00Z Denotational semantics and domain theory Goslett, J. Hulley, H Melton, A http://hdl.handle.net/10500/24124 2018-06-06T11:51:39Z 1993-01-01T00:00:00Z Denotational semantics and domain theory Goslett, J.; Hulley, H; Melton, A This tutorial is an introduction to denotational semantics and domain theory. For this reason the presentation is not entirely rigorous, with some proofs being omitted and certain simplifying assumptions being made. Instead, the emphasis here has been on satisfying the computational intuition of the reader - dwelling too long on the mathematical aspects of semantic domains is not always satisfying to somebody attempting to ascertain why these structures are relevant to computer science in the first place. Thus, we have started right at the beginning by discussing the concepts of syntax and semantics, and we have attempted to build the mathematical theory of domains upon this computational foundation in a fluid, intuitive and informal manner. In Section 1 and Section 2 we begin with brief descriptions of the syntax and semantics of computer languages, the roles these notions play in computer science, and how they interact in the quest for a formal methodology for computer programming. Section 3 provides an introduction to denotational semantics in particular - this being illustrated by a very simple example. In Section 4 we get down to the business of defining a language which can be recognised as something approximating a real computer language. Here we also endow this language (which can be found in ) with a denotational description. We have attempted to explain why the semantics presented for our toy language should seem natural to the reader. In Sections 5-7 we begin to explore the mathematical complexities of domain theory. Our motivation for introducing all this new theory is the search for a denotational description of the 'while'-loop in our example programming language. We conclude in Section 8 with a discussion of parallelism, non-determinism, and the new demands which these complications make of the theory developed up to then. For more advanced presentations of denotational semantics and domain theory, we recommend [3, 4, 6, 7, 10]. 1993-01-01T00:00:00Z Deduction systems based on resolution Eisinger, N Ohlbach, HJ http://hdl.handle.net/10500/24123 2018-07-02T09:53:45Z 1993-01-01T00:00:00Z Deduction systems based on resolution Eisinger, N; Ohlbach, HJ A general theory of deduction systems is presented The theory is illustrated with deduction systems based on the resolution calculus, in particular with clause graphs. This theory distinguishes four constituents of a deduction system: • the logic, which establishes a notion of semantic entailment; • the calculus, whose rules of inference provide the syntactic counterpart of entailment; • the logical state transition system, which determines the representation of formulae or sets of formulae together with their interrelationships, and also may allow additional operations reducing the search space; • the control, which comprises the criteria used to choose the most promising from among all applicable inference steps. Much of the standard material on resolution is presented in this framework. For the last two levels many alternatives are discussed. Appropriately adjusted notions of soundness, completeness, confluence, and Noetherianness are introduced in order to characterize the properties of particular deduction systems. For more complex deduction systems, where logical and topological phenomena interleave, such properties can be far from obvious. 1993-01-01T00:00:00Z