the proceedings contain 20 papers. the special focus in this conference is on algebraic and logicprogramming. the topics include: Concurrent constraint programming;specifications using multiple-conclusion logic progr...
ISBN:
(纸本)9783540584315
the proceedings contain 20 papers. the special focus in this conference is on algebraic and logicprogramming. the topics include: Concurrent constraint programming;specifications using multiple-conclusion logic programs;viewing a program transformation system at work;proving implications by algebraic approximation;sufficient completeness and parameterized proofs by induction;proving behavioural theorems with standard first-order logic;compositional analysis for equational horn programs;equation solving in projective planes and planar ternary rings;concurrent logicprogramming as uniform linear proofs;three-valued completion for abductive logic programs;a sequential reduction strategy;on modularity of termination and confluence properties of conditional rewrite systems;syntactical analysis of total termination;logic programs as term rewriting systems;higher-order minimal function graphs;reasoning about layered, wildcard and product patterns;preserving universal termination through unfold/fold and a logic for variable aliasing in logic programs.
the proceedings contain 34 papers. the special focus in this conference is on logicprogramming and Nonmonotonic Reasoning. the topics include: Strong and weak constraints in disjunctive datalog;non-monotonic reasonin...
ISBN:
(纸本)9783540632559
the proceedings contain 34 papers. the special focus in this conference is on logicprogramming and Nonmonotonic Reasoning. the topics include: Strong and weak constraints in disjunctive datalog;non-monotonic reasoning with quantified Boolean constraints;complexity of only knowing;affordable classes of normal logic programs;automated reasoning with non-monotonic logics;simulations between programs as cellular automata;separating disbeliefs from beliefs in autoepistemic reasoning;resolution for skeptical stable semantics;computing non-ground representations of stable models;industry needs for integrated information services;towards a systematic approach to representing knowledge in declarative logicprogramming;a paraconsistent semantics with contradiction support detection;a general framework for revising non-monotonic theories;modular logicprogramming and generalized quantifiers;programs with universally quantified embedded implications;generalized query answering in disjunctive deductive databases;towards a disjunctive logicprogramming system;a deductive system for non-monotonic reasoning;flexible solutions to complex problems;an implementation of the stable model and well-founded semantics for normal lp;an implementation platform for query-answering in default logics and the x-ray system, its implementation and evaluation.
the proceedings contains 18 papers. Topics discussed include simulation models of short rotation forestry, willow wood properties, production and economy, poplar cultivation, seasonal amount, growth and depth distribu...
详细信息
the proceedings contains 18 papers. Topics discussed include simulation models of short rotation forestry, willow wood properties, production and economy, poplar cultivation, seasonal amount, growth and depth distribution of roots, demographic studies of canopy development, biomass fuel, and coppice culture.
Finite maps or finite relations between infinite sets do not even form a category, since the necessary identities are not finite. We show relation-algebraic extensions of semigroupoids where the operations that would ...
详细信息
Finite maps or finite relations between infinite sets do not even form a category, since the necessary identities are not finite. We show relation-algebraic extensions of semigroupoids where the operations that would produce infinite results have been replaced with variants that preserve finiteness, but still satisfy useful algebraic laws. the resulting theories allow calculational reasoning in the relation-algebraic style with only minor sacrifices;our emphasis on generality even provides some concepts in theories where they had not been available before. the semigroupoid theories presented in this paper also can directly guide library interface design and thus be used for principled relation-algebraicprogramming;an example implementation in Haskell allows manipulating finite binary relations as data in a point-free relation-algebraicprogramming style that integrates naturally withthe current Haskell collection types. this approach enables seamless integration of relation-algebraic formulations to provide elegant solutions of problems that, with different data organisation, are awkward to tackle. (C) 2007 Elsevier Inc. All rights reserved.
We present an algebraic embedding of Neighbourhood logic (NL) into the framework of semirings which yields various simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our fra...
详细信息
We present an algebraic embedding of Neighbourhood logic (NL) into the framework of semirings which yields various simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our framework, and Galois connections produce properties for free. A further simplification is achieved, since the semiring methods used are easy and fairly standard. Moreover, this embedding allows us to reuse knowledge from Neighbourhood logic in other areas of Computer Science. Since in its original axiomatisation the logic cannot handle intervals of infinite length and therefore not fully model and specify reactive and hybrid systems, using lazy semirings we introduce an extension of NL to intervals of finite and infinite length. Furthermore, we discuss connections between the (extended) logic and other application areas, like Allen's thirteen relations between intervals, the branching time temporal logic CTL* and hybrid systems. (C) 2007 Elsevier Inc. All rights reserved.
the theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logicprogramming languages. Two such languages, lambda Prolog and its linear logic refinement, Lolli [15], provide...
详细信息
the theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logicprogramming languages. Two such languages, lambda Prolog and its linear logic refinement, Lolli [15], provide for various forms of abstraction (modules, abstract data types, and higher-order programming) but lack primitives for concurrency. the logicprogramming language, LO (Linear Objects) [2] provides some primitives for concurrency but lacks abstraction mechanisms. In this paper we present Forum, a logicprogramming presentation of all of linear logicthat modularly extends lambda Prolog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concurrency. To illustrate the new expressive strengths of Forum, we specify in it a sequent calculus proof system and the operational semantics of a programming language that incorporates references and concurrency. We also show that the meta theory of linear logic can be used to prove properties of the object-languages specified in Forum.
this paper introduces a logic for a class of properties - in particular variable aliasing - used in static analysis of logic programs. the logic is shown to be sound, complete and decidable. Moreover, it is illustrate...
详细信息
In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated withthe Console et al. two-valued completion semantics. the semantics is a generalizat...
详细信息
In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated withthe Console et al. two-valued completion semantics. the semantics is a generalization of Kunen's completion semantics for general logic programs, which is known to correspond very well to a class of effective proof procedures for general logic programs. Secondly, we propose a proof procedure for abductive logic programs, which is a generalization of a proof procedure for general logic programs based on constructive negation. this proof procedure is sound and complete with respect to the proposed semantics. By generalizing a number of results on general logic programs to the class of abductive logic programs, we present further evidence for the idea that limited forms of abduction can be added quite naturally to general logic programs.
暂无评论