In this paper we present a binding-time analysis for the logicprogramming language Mercury. Binding-time analysis is a key analysis needed to perform off-line program specialisation. Our analysis deals withthe highe...
详细信息
ISBN:
(纸本)3540412859
In this paper we present a binding-time analysis for the logicprogramming language Mercury. Binding-time analysis is a key analysis needed to perform off-line program specialisation. Our analysis deals withthe higher-order aspects of Mercury, and is formulated by means of constraint normalisation. this allows (at least part of) the analysis to be performed on a modular basis.
We handle finite graphs in two ways, as relational structures on the one hand, and as algebraic objects, i.e., as elements of algebras, based on graph operations on the other.
ISBN:
(纸本)3540412859
We handle finite graphs in two ways, as relational structures on the one hand, and as algebraic objects, i.e., as elements of algebras, based on graph operations on the other.
作者：
de Groote, PINRIA
LORIA UMR 7503 F-54506 Vandoeuvre Les Nancy France
We reduce the provability of fragments of multiplicative linear logic to matching problems consisting in finding a one-one-correspondence between two sets of first-order terms together with a unifier that equates the ...
详细信息
ISBN:
(纸本)3540412859
We reduce the provability of fragments of multiplicative linear logic to matching problems consisting in finding a one-one-correspondence between two sets of first-order terms together with a unifier that equates the corresponding terms. According to the kind of structure to which these first-order terms belong our matching problem corresponds to provability in the implicative fragment of multiplicative linear logic, in the Lambek calculus, or in the non-associative Lambek calculus.
this paper presents a tool for proving safety properties of Lustre programs in PVS, based on continuous induction. the tool applies off-line a repeated induction strategy and generates proof obligations left to PVS. W...
详细信息
ISBN:
(纸本)3540412859
this paper presents a tool for proving safety properties of Lustre programs in PVS, based on continuous induction. the tool applies off-line a repeated induction strategy and generates proof obligations left to PVS. We show on examples how it avoids some drawbacks of co-induction which needs to consider "absent elements" in the case of clocked streams.
We prove that a particular superposition based inference operator decides a fragment of clause logic with equality, called OCC1N(g)(=),. We also show that the theorem prover SPASS not only implements the corresponding...
详细信息
ISBN:
(纸本)3540412859
We prove that a particular superposition based inference operator decides a fragment of clause logic with equality, called OCC1N(g)(=),. We also show that the theorem prover SPASS not only implements the corresponding operator but also generates standard descriptions of unique term models for all satisfiable clause sets in OCC1N(g)(=),.
the main goal of the paper is to propose a tool for a semantic specification of program updates (in the context of dynamic logicprogramming paradigm). A notion of Kripke structure K-P associated with a generalized lo...
详细信息
ISBN:
(纸本)3540412859
the main goal of the paper is to propose a tool for a semantic specification of program updates (in the context of dynamic logicprogramming paradigm). A notion of Kripke structure K-P associated with a generalized logic program P is introduced. It is shown that some paths in K-P specify stable models of P and vice versa, to each stable model of P corresponds a path in K-P. An operation on Kripke structures is defined: for Kripke structures K-P and K-U associated with P (the original program) and U (the updating program), respectively, a Kripke structure K-Pcircle plusU is constructed. K-Pcircle plusU specifies (in a reasonable sense) a set of updates of P by U. there is a variety of possibilities for a selection of an updated program.
In this paper we define a semantic foundation for an abstract interpretation approach to universal termination and we develop a new abstract domain useful for termination analysis. Based on this approximation we defin...
详细信息
ISBN:
(纸本)3540412859
In this paper we define a semantic foundation for an abstract interpretation approach to universal termination and we develop a new abstract domain useful for termination analysis. Based on this approximation we define a method which is able to detect classes of goals which universally terminate (with a fair selection rule). We also define a method which is able to characterize classes of programs and goals for which depth-first search is fair.
Withthe aim of automatically reasoning with spatial aspects in a cognitive way, several qualitative models have been developed in recent years. However, there is no model to reason with several spatial aspects in a u...
详细信息
Withthe aim of automatically reasoning with spatial aspects in a cognitive way, several qualitative models have been developed in recent years. However, there is no model to reason with several spatial aspects in a uniform way. Moreover, most of these models simplify spatial objects to points. In this paper we present the use of constraint logicprogramming instantiated to finite domains extended with constraint handling rules as a tool for successfully integrating the qualitative concepts of orientation, distance, and cardinal directions, using points as well as extended objects as a primitive of reasoning. the resulting model has been applied to build a demonstrator: a qualitative navigation simulator on the structured environment of our city. (C) 2000 John Wiley & Sons, Inc.
We present a procedure for deciding (database) query containment under constraints. the technique is to extend the logic DLR with an ABox, and to transform query subsumption problems into DLR ABox satisfiability probl...
详细信息
ISBN:
(纸本)3540412859
We present a procedure for deciding (database) query containment under constraints. the technique is to extend the logic DLR with an ABox, and to transform query subsumption problems into DLR ABox satisfiability problems. Such problems can then be decided, via a reification transformation, using a highly optimised reasoner for the SHIQ description logic. We use a simple example to support our hypothesis that this procedure will work well with realistic problems.
In this paper we demonstrate how a default theory, expressed through a set of conditional defaults that the agent possesses, can be traduced into extended logic programs. Additionally, the proposed trans-lation allows...
详细信息
暂无评论