this paper describes an algorithm for the code generation of determinacy testing for nondeterminate flat concurrent logicprogramming languages. Languages such as Andorra and Pandora require that procedure invocations...
详细信息
ISBN:
(纸本)0262560585
this paper describes an algorithm for the code generation of determinacy testing for nondeterminate flat concurrent logicprogramming languages. Languages such as Andorra and Pandora require that procedure invocations suspend if there is more than one candidate clause potentially satisfying the goal. the algorithm described has been developed specifically for a variant of flat Pandora based on FGHC, although the concepts are general. We have extended Kliger and Shapiro's decision-graph construction algorithm to compile ``don't know'' procedures which must suspend for nondeterminate goal invocation. the determinacy test is compiled into a decision graph quite different from those of committed-choice procedures, but we argue that in most cases, the same low space complexity is retained.
Withthe emergence of formal specification methods, it becomes possible to develop new approaches for ``black-box'' testing. this paper addresses this problem in the particular case of algebraic specifications...
详细信息
ISBN:
(纸本)0262560585
Withthe emergence of formal specification methods, it becomes possible to develop new approaches for ``black-box'' testing. this paper addresses this problem in the particular case of algebraic specifications. We provide a way to automate test data set selection from the algebraic specification of a program using logicprogramming techniques. First, we introduce a black box testing theory based on Algebraic Specifications. then some specific selection strategies, based on sensible selection hypotheses, are developed. they are based on a decomposition into uniformity subdomains via the axioms of the specification. these strategies are implemented using logicprogramming. A system is presented which, given an algebraic specification and some hints on the selection given by the user, finds the uniformity subdomains and generates the corresponding test data sets.
In this paper we propose a new approach towards amalgamating logicprogramming and functional programming. the proposed language AMLOG-E is based on equational definite clauses. the difference, wrt. other related appr...
详细信息
ISBN:
(纸本)0262560585
In this paper we propose a new approach towards amalgamating logicprogramming and functional programming. the proposed language AMLOG-E is based on equational definite clauses. the difference, wrt. other related approaches, lies in that an AMLOG-E program is viewed as defining a (conditional) reduction relation which is different from that of a (conditional) TRS. the proposed computation mechanism, c-superposition, does not require the unifiability withthe head of a program clause as a pre-requisite for rule application. the soundness and completeness of the language is shown. It is also shown that the scope of the language is larger than those of similar approaches.
A logic program is considered as an abductive framework with negative literals as hypotheses. We define a simple declarative semantics for abduction and show that the new semantics captures, generalizes and unifies di...
详细信息
A logic program is considered as an abductive framework with negative literals as hypotheses. We define a simple declarative semantics for abduction and show that the new semantics captures, generalizes and unifies different semantic concepts (e.g. well-founded models, stable models) in logicprogramming. We study the operational semantics of abduction, and prove the soundness of the Eshghi and Kowalski's abductive procedure with respect to our new declarative semantics.
We introduce polymorphically typed logic programs, an integration of a polymorphic type system withlogic programs. Such programs incorporate parametric predicates, which are parameterized by types. the type system ac...
详细信息
ISBN:
(纸本)0262560585
We introduce polymorphically typed logic programs, an integration of a polymorphic type system withlogic programs. Such programs incorporate parametric predicates, which are parameterized by types. the type system accommodates both subtypes and parametric polymorphism. the denotation of a typed logic program is given via its type completion, a transformation that incorporates explicit type conditions into a parametric logic program. the result of the transformation is a restricted form of a HiLog program. We give fixpoint semantics to our language (actually to full HiLog). We define a notion of well-typing, which relates type declarations for predicates in the program to an approximation of the denotation of the type completed program. We present a type-checking algorithm for verifying that a program is indeed well-typed.
We develop a perfect model semantics for logic programs with negation and equality. Our approach is based on ordered rewriting, a fundamental technique used in equational programming. A logic program in our sense is a...
详细信息
ISBN:
(纸本)0262560585
We develop a perfect model semantics for logic programs with negation and equality. Our approach is based on ordered rewriting, a fundamental technique used in equational programming. A logic program in our sense is a set of first-order clauses with equality together with a well-founded ordering on terms and atoms. We show that any consistent logic program has a unique perfect model, provided the ordering is total on ground expressions. the key to this result is a notion of saturation of a set of formulas (under certain inference rules) together with a related concept of redundancy. Our techniques can be applied to Prolog-programs (without equality), in which case a class of programs can be characterized via the notion of stratification up to redundancy for which unique perfect models exist. this extends previous results on (local and weak) stratification.
We investigate the declarative semantics of logic programs with negation. First, we propose the extended well-founded model semantics. then we establish three important criteria of declarative semantics for logic prog...
详细信息
We investigate the declarative semantics of logic programs with negation. First, we propose the extended well-founded model semantics. then we establish three important criteria of declarative semantics for logic programs. Finally we justify our extension through the comparison of different semantics.
CHIP is a constraint logicprogramming language developed at ECRC. It extends the usual Prolog-like logic languages in two ways. First, in addition to the Herbrand universe, it introduces three new computation domains...
详细信息
ISBN:
(纸本)0262560585
CHIP is a constraint logicprogramming language developed at ECRC. It extends the usual Prolog-like logic languages in two ways. First, in addition to the Herbrand universe, it introduces three new computation domains: finite domains, boolean terms and linear rational terms. Second, it provides powerful control structures like the extension of coroutining and demon rules. Different prototype implementations of CHIP have been developed at ECRC since 1986. Based upon this experience a new system, the CHIP compiler, was developed and has now been completed. It embeds the three computation domains withtheir related constraint solving techniques and control structures in the Prolog SEPIA compiler. this paper gives an overview of the architecture of the CHIP compiler. We review the design of the CHIP kernel which extends the usual Prolog engine with a set of mechanisms to take the different extensions into account at a low system level.
In higher-order logicprogramming, set abstractions are often used for auxiliary predicates that do not have to be named. this paper presents a simple logic for reasoning about set abstractions. the semantics is more ...
详细信息
In higher-order logicprogramming, set abstractions are often used for auxiliary predicates that do not have to be named. this paper presents a simple logic for reasoning about set abstractions. the semantics is more tractable in the sense that the equality of terms corresponds to α-equivalence. A strongly restricted variant of β-reduction, called top β-reduction, is introduced for evaluating set memberships as atomic formulas. this enables us to incorporate set abstractions into a logic without the complications of higher-order functions.
暂无评论