Fundamenta Informaticae

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.

This paper addresses the problem of updating knowledge encoded in the form of a logic program. Our approach is based upon the idea of executing a basic update by directly modifying the truth valuation of the (intensionally or extensionally defined) atom which is the object of an update. The modifications propagate, in a recursive fashion, to the truth valuations of atoms depending on the updated one. An update language is defined around this central idea. The language is built upon two basic update operators, respectively denoting insertion and deletion of a positive literal (atom). Several structures are defined for combining basic updates into complex ones and controlling the execution flow.

We propose to use the logic of only knowing (OL) by Levesque [10] as a unified framework that encompasses various non-monotonic formalisms and logic programming. OL is a modal logic which can be used to formalize an agent's introspective reasoning and to answer epistemic queries to databases. The OL logic allows one to formally express the statement “α is all I know” (in symbols, Oα) and to perform inferencing based on only-knowing, which is very useful for commonsense reasoning. Another nice thing about the OL logic is that it has a clear model-theoretic semantics and a simple proof theory, which is sound for the quantificational case, and both sound and complete for the prepositional case. We establish the relations between OL and various non-monotonic logics (such as default logic, circumscription) and logic programming, thus extending the existing works relating the OL logic with other non-monotonic reasoning formalisms (e.g., Levesque showed that autoepistemic logic can be embeded in OL). This is accomplished by finding the connection between OL and MBNF, the logic of Minimal Belief and Negation as Failure proposed by Lifschitz [12, 13], which is known to have close relationship with logic programming and other non-monotonic logics. Our results show that OL can be used as a unified framework to compare different non-monotonic formalisms based on the same domain.

Semantic hyper-linking has recently been proposed as a way to use semantics in an instance-based theorem prover. The basic procedure is to use semantics to help generate ground instances of the input clauses until the ground clause set is unsatisfiable. If the ground set is satisfiable, models are constructed periodically to guide generation of new ground instances and change the models, until no model can be constructed and a proof is found. In this paper we discuss some model finding strategies that can generate useful ground instances, without using semantics, to change the ground models. We show that such strategies are helpful and will not increase the search space of semantic hyper-linking. They also retain the completeness of semantic hyper-linking. In addition, since using semantics is often expensive and semantics is not used in those model finding strategies, they help to find proofs earlier and faster.

We consider means for adapting classical deduction techniques to multiple-valued logics. Some recent work in this area, including our own, utilizes signs (subsets of the set of truth values). In this paper we develop a language of signed formulas that may be interpreted as a meta-level logic. Questions not expressible in the underlying logic are easily expressed in this meta-logic, and they may be answered with classical techniques because the logic is classical in nature. We illustrate the applicability of classical techniques by adapting resolution, path resolution, and path dissolution to signed formulas. The meta-logic admits a version of Herbrand's Theorem, so that these results extend naturally to the first order case. The fact that annotated logics are a special case of signed formulas is briefly illustrated.