the proceedings contain 30 papers. the special focus in this conference is on Nonmononic reasoning and Descriptive complexity. the topics include: On the complexity of theory curbing;graph operations and monadic secon...
ISBN:
(纸本)3540412859
the proceedings contain 30 papers. the special focus in this conference is on Nonmononic reasoning and Descriptive complexity. the topics include: On the complexity of theory curbing;graph operations and monadic second-order logic;efficient first order functional program interpreter with time bound certifications;encoding temporal logics in executable Z;behavioural constructor implementation for regular algebras;an extensible proof text editor;a tactic language for the system Coq;proof simplification for model generation and its applications;compiling and verifying security protocols;equational binary decision diagrams;a PVS proof obligation generator for lustre programs;efficient structural information analysis for real CLP languages;playing logic programs withthe alpha-beta algorithm;logicprogramming approaches for representing and solving constraint satisfaction problems;proof-search in implicative linear logic as a matching problem;a new model construction for the polymorphic lambda calculus;church’s lambda delta calculus;querying inconsistent databases;static reduction analysis for imperative object oriented languages;an abstract interpretation approach to termination of logic programs and using an abstract representation to specialize functional logic programs.
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.
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.
作者：
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.
We describe a method for abbreviating an analytic classical first-order logic by the introduction of a lemma. Our is based on first computing a compressed representation of present in the analytic proof and then a cut...
详细信息
ISBN:
(纸本)9783642287176
We describe a method for abbreviating an analytic classical first-order logic by the introduction of a lemma. Our is based on first computing a compressed representation of present in the analytic proof and then a cut-formula that
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.
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.
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.
Alpha-Beta is a well known optimized algorithm used to compute the values of classical combinatorial games, like chess and checkers. the known proofs of correctness of Alpha-Beta do rely on very specific properties of...
详细信息
Many logicprogramming based approaches can be used to describe and solve combinatorial search problems. On the one hand there is constraint logicprogramming which computes a solution as an answer substitution to a q...
详细信息
ISBN:
(纸本)3540412859
Many logicprogramming based approaches can be used to describe and solve combinatorial search problems. On the one hand there is constraint logicprogramming which computes a solution as an answer substitution to a query containing the variables of the constraint satisfaction problem. On the other hand there are systems based on stable model semantics, abductive systems, and first order logic model generators which compute solutions as models of some theory. this paper compares these different approaches from the point of view of knowledge representation (how declarative are the programs) and from the point of view of performance (how good are they at solving typical problems).
暂无评论