We propose a new implementation of logicprogramming with higher-order terms. In order to illustrate the properties of our implementation, we apply the coding of lists as functions to the context of logicprogramming....
详细信息
ISBN:
(纸本)0262560585
We propose a new implementation of logicprogramming with higher-order terms. In order to illustrate the properties of our implementation, we apply the coding of lists as functions to the context of logicprogramming. As a side-effect, we show that higher-order unification is a good tool for manipulating the function-lists. It appears that the efficiency of the program thus obtained relies critically upon the implementation of higher-order operations (unification and reduction). In particular, we show that a good choice for data-structures and reduction strategy yields a linear naive reverse.
there have been several recent proposals for coping with uncertainty and vagueness in automated theorem proving and in logicprogramming, based on fuzzy logic or on other approaches, which are briefly analyzed in the ...
详细信息
ISBN:
(纸本)0262560585
there have been several recent proposals for coping with uncertainty and vagueness in automated theorem proving and in logicprogramming, based on fuzzy logic or on other approaches, which are briefly analyzed in the paper. A new approach to logicprogramming with weighted clauses, based on possibility theory is proposed. Possibilistic logic is an extension of classical logic where one manipulates propositional or first-order formulae weighted by lower bounds of possibility or necessity degrees. the extension of the resolution principle to possibilistic logic provides us with a basic tool for theorem proving under uncertainty. In this paper we are going one step further by beginning to investigate logicprogramming techniques for possibilistic logic.
We develop a novel dataflow analysis for the detection of ``possible'' suspension of concurrent logic programs. the analysis is conceptually simple and easy to justify because it is based directly on the trans...
详细信息
ISBN:
(纸本)0262560585
We develop a novel dataflow analysis for the detection of ``possible'' suspension of concurrent logic programs. the analysis is conceptually simple and easy to justify because it is based directly on the transition system semantics of concurrent logic programs. A naive analysis must consider all scheduling policies. However, we prove that for our analysis it suffices to consider only one scheduling policy. this allows for efficient implementation. the analysis is demonstrated for the concurrent logic language FCP(:) and shown to provide promising results.
It is shown that higher-order unification procedures for higher-order type systems such as logical Framework can be used as a theorem proving procedure if projection is also allowed on flexible-flexible pairs. In part...
详细信息
ISBN:
(纸本)0262560585
It is shown that higher-order unification procedures for higher-order type systems such as logical Framework can be used as a theorem proving procedure if projection is also allowed on flexible-flexible pairs. In particular, SLD-resolution of Prolog can be completely simulated with a slight additional control for selecting equations in higher-order unification. We also derive a Prolog interpreter from a higher-order unification procedure for logical Framework by program transformation.
the unification of simply typed λ-terms modulo the rules of β- and η-conversions is often called ``higher-order'' unification because of the possible presence of variables of functional type. this kind of u...
详细信息
ISBN:
(纸本)0262560585
the unification of simply typed λ-terms modulo the rules of β- and η-conversions is often called ``higher-order'' unification because of the possible presence of variables of functional type. this kind of unification is undecidable in general and if unifiers exist, most general unifiers may not exist. In this paper, we show that such unification problems can be coded as a query of the logicprogramming language Lλ in a natural and clear fashion. In a sense, the translation only involves explicitly axiomatizing in Lλthe notions of equality and substitution of the simply typed λ-calculus: the rest of the unification process can be viewed as simply an interpreter of Lλ searching for proofs using those axioms.
the extension of s-models from definite to general programs leads to the introduction of a notion complementary to that of most general unifier. For this purpose, we draw upon the work done on constructive negation an...
详细信息
ISBN:
(纸本)0262560585
the extension of s-models from definite to general programs leads to the introduction of a notion complementary to that of most general unifier. For this purpose, we draw upon the work done on constructive negation and define the notion of most general disunifier. the atoms in the extended s-models are then constrained by sets of inequalities in a solved form which we define both declaratively and procedurally. We apply the resulting framework to stratified programs and, by a standard fixpoint construction, we obtain a single model which is ``universal'' in the sense that it encodes the whole class of representative models for stratified programs.
We outline methods of compiling recursive procedures in Prolog to yield code which is close to that of imperative languages. Recursion is compiled into iteration which keeps loop invariants unchanged and uses destruct...
详细信息
ISBN:
(纸本)0262560585
We outline methods of compiling recursive procedures in Prolog to yield code which is close to that of imperative languages. Recursion is compiled into iteration which keeps loop invariants unchanged and uses destructive assignment on the stack variables. We also identify various recursion types, depending on the stack frame type which is involved, namely environments, choice points and suspended goals.
Extended logic programs were proposed by Gelfond and Lifschitz (1990) as logic programs with classical negation capable of expressing incomplete knowledge. their work is expanded in this paper to deal with broader cla...
详细信息
ISBN:
(纸本)0262560585
Extended logic programs were proposed by Gelfond and Lifschitz (1990) as logic programs with classical negation capable of expressing incomplete knowledge. their work is expanded in this paper to deal with broader classes of commonsense knowledge. Like Poole's framework, some clauses are dealt with as assumptions distinct from a theory about the world and are used to augment the theory. this theory formation framework can be used for default reasoning, abduction and inconsistency resolution. We also show a translation of the framework to an extended logic program whose answer sets correspond to consistent belief sets of augmented theories.
For the programming environment of a parallel logicprogramming language, it is an important problem to develop a debugger. However it is difficult to debug parallel programs by observing their execution traces. Using...
详细信息
In this paper an axiomatic semantics of logic programs is defined and proved sound. the main novelty consists in the treatment of the unification process as a predicate relation, through a system of correctness rules....
详细信息
ISBN:
(纸本)0262560585
In this paper an axiomatic semantics of logic programs is defined and proved sound. the main novelty consists in the treatment of the unification process as a predicate relation, through a system of correctness rules. this semantics allows to prove, in a Hoare-like way, the partial correctness of a logic program with respect to a goal and a specification. A criterion to prove termination (total correctness) is given and its soundness is proved. We show also how finite failure property is equivalent to the total correctness of a suitable specification and thus it can be proved by using the axiomatic semantics and the termination criterion. An execution mechanism using the Prolog selection rule and arbitrary search strategy (e.g. OR-parallelism or Prolog backtraking) is assumed.
暂无评论