From logic design to logic programming. Theorem proving techniques and P- functions (Q1099944)

This book presents so called P-functions, which are described earlier by one of the authors. Such P-functions are pairs of logical statements. Each first component of such a pair gives some specification and each second component gives a corresponding implementation of some program or another construct. Each set of P-functions can be extended by the result of a logical deduction on certain elements of the set. Such a logical deduction transforms both the first component and the second component. Of course the deductions have to be consistent, i.e. the transformations on both components correspond to each other. The authors use this framework on several items. They describe an application of these functions to a systematic way of programming development. For a set of situations they describe what the output function of the program is. They describe tranformations that take the conjunction or disjunction of two situations and what the derived output should be in that case. After giving these preconditions they transform the set of P-functions in such a way that the first component becomes equal to truth. For this pair the second component is then equal to the program that computes the function in all cases. Another application lies in the field of natural language understanding. There they show how sentences can be transformed into the structures of the LFG-semantics of (a part of) English. They also see possibilities for using it with a simple grammar for a natural language for text editors.