Search

There is a close relationship between word unification and second-order unification. This similarity has been exploited, for instance, in order to prove decidability of monadic second-order unification and decidability of linear second-order unification when no second-order variable occurs more than twice. The attempt to prove the second result for (nonlinear) second-order unification failed and led instead to a natural reduction from simultaneous rigid E-unification to this second-order unification. This reduction is the first main result of this paper, and it is the starting point for proving some novel results about the undecidability of second-order unification presented in the rest of the paper. We prove that second-order unification is undecidablein the following three cases: (1) each second-order variable occurs at most twice and there are only two second-order variables; (2) there is only one second-order variable and it is unary; (3) the following conditions (i)–(iv) hold for some fixed integer n: (i) the arguments of all second-order variables are ground terms of size

Requirements capture is a term used in software engineering, referring to the process of obtaining a problem description – a high level account of the problem which a user wants to solve. This description is then used to control the generation of a program appropriate to the solution of this problem. Reliable requirements capture is seen as a key component of future automated program construction systems, since even small amounts of information about the type of problem being tackled can often vastly reduce the space of appropriate application programs. Many special purpose requirements capture systems exist but few of these are logic based and all of them operate in tightly constrained domains. In previous research, we have used a combination of order sorted logic (for problem description) and Prolog (for the generated program) in an attempt to provide a more general purpose requirements capture system. However, in our earlier systems the connection between the problem description and the resulting program was obtained using ad hoc methods requiring considerable amounts of domain–specific information, thus limiting the domain of application of the system. We are experimenting with languages which provide a formal connection between problem description and application program, thus eliminating the need for domain–specific information in the translation process. This paper introduces a formal language for requirements capture which bridges the gap between an order sorted logic of problem description and the Prolog programming language. The meaning of a Prolog predicate is often characterised according to the set of bindings which can be obtained for its arguments. It is therefore possible to develop a hierarchical arrangement of predicates by comparing the sets of results obtained for stipulated variables. Using this hierarchical structure, we provide proof rules which may be used to support part of the requirements capture process. We describe the notation used for the refinement lattice; define its relationship to Prolog and demonstrate how the language can be used to support requirements capture. An interactive system for extracting Prolog programs from our refinement hierarchies, using an algorithm similar to the one described in this paper, has been implemented.

In this article we propose an extension of term rewriting techniques to automate the deduction in monotone pre-order theories. To prove an inclusionabfrom a given setIof them, we generate fromI, using a completion procedure, abi-rewrite system, that is, a pair of rewrite relations and , and seek a common termcsuch thatacandbc. Each component of the bi-rewrite system and is allowed to be a subset of the corresponding inclusion relation or defined by the theory ofI. In order to assure the decidability and completeness of such proof procedure we study the termination and commutation of and . The proof of the commutation property is based on a critical pair lemma, using anextendeddefinition of critical pair. We also extend the existing techniques of rewriting modulo equalities to bi-rewriting modulo a set of inclusions. Although we center our attention on the completion process á la Knuth–Bendix, the same notion of extended critical pairs is suitable to be applied to the so-called unfailing completion procedures. The completion process is illustrated by means of an example corresponding to the theory of the union operator. We show that confluence ofextendedcritical pairs may be ensured addingrule schemes. Such rule schemes contain variables denoting schemes of expressions, instead of expressions. We propose the use of thelinear second-order typedλ-calculustocodifythese expression schemes. Although the general second-order unification problem is only semi-decidable, the second-order unification problems we need to solve during the completion process are decidable.