the proceedings contain 24 papers. the special focus in this conference is on logicprogramming and automatedreasoning. the topics include: Generalization and reuse of tactic proofs;program tactics and logic tactics;...
ISBN:
(纸本)9783540582168
the proceedings contain 24 papers. the special focus in this conference is on logicprogramming and automatedreasoning. the topics include: Generalization and reuse of tactic proofs;program tactics and logic tactics;proof plans for the correction of false conjectures;on the value of antiprenexing;implementing a finite-domain CLP-language on top of prolog;logical closures;higher-order rigid e-unification;program extraction in a logical framework setting;higher-order abstract syntax with induction in coq;towards efficient calculi for resource-oriented deductive planning;a logicprogramming framework for the abductive inference of intentions in cooperative dialogues;constraint logicprogramming in the sequent calculus;on conditional rewrite systems with extra variables and deterministic logic programs;a bottom-up reconstruction of the well-founded semantics for disjunctive logic programs;an efficient computation of the extended generalized closed world assumption by support-for-negation sets;multi-SLD resolution;on anti-links;a generic declarative diagnoser for normal logic programs;a kind of achievement by parts method and projection in temporal logicprogramming.
In this paper, we are developing a new logical semantics of CLP. It is shown that CLP is based on an amalgamated logic embedding the entailment relation of constraints into a fragment of intuitionistic logic. Constrai...
详细信息
In the past, tactics have been mostly implemented as programs written in some programming language, e.g. ML. We call the tactics of this kind, Program Tactics. In this paper we present a first order classical metatheo...
详细信息
Uniform proof procedures for hereditary Harrop formulae have been proposed as a foundation for logicprogramming. A non-standard approach to defining hereditary Harrop formula is given, allowing quantification over pr...
详细信息
We study deterministic conditional rewrite systems, i.e. conditional rewrite systems where the extra variables are not totally free but ‘input bounded’. If such a system R is quasi-reductive then →R is decidable an...
详细信息
In this paper we propose a general logicprogramming framework allowing the recognition of plans and intentions behind speech acts through abductive reasoning. these inferences enables each agent to have an active par...
详细信息
In this paper we develop a generic declarative diagnoser for normal logic programs that is based on tree search. the soundness and the completeness of the diagnoser are proved. the diagnoser is generic in that it can ...
详细信息
A constraint logicprogramming system for the domain of complex functions is described. the intended users of the language are scientist and engineers who often reason/compute with constraints over complex functions, ...
详细信息
In this paper, we examine the effect of antiprenexing on the proof length if resolution deduction concepts are applied. Roughly speaking, our version of antiprenexing moves ∀-quantifiers downward in the formula tree w...
详细信息
暂无评论