The search for an appropriate characterization of negation as failure inlogic programs in the mid 1980s led to several proposals. Amongst them the stable model semantics -later referred to as answer set semantics, and...
详细信息
The search for an appropriate characterization of negation as failure inlogic programs in the mid 1980s led to several proposals. Amongst them the stable model semantics -later referred to as answer set semantics, and the well-founded semantics are the most popular andwidely referred ones. According to the latest (September 2002) list of most cited source documentsin the CiteSeer database (http://***) the original stable model semantics paper(Gelfond and Lifschitz, 1988) is ranked 10th with 649 citations and the well-founded semantics paper(Van Gelder et al., 1991) is ranked 70th with 306 citations. Since 1988 - when stable modelssemantics was proposed - there has been a large body of work centered around logic programs withanswer set semantics covering topics such as: systematic program development, systematic programanalysis, knowledge representation, declarative problem solving, answer set computing algorithms,complexity and expressiveness, answer set computing systems, relation with other nonmonotonic andknowledge representation formalisms, and applications to various tasks. This large body ofbuilding-block results makes logicprogramming with answer sets (sometimes called A-Prolog orAnsProlog) an attractive and suitable language for declarative programming, knowledgerepresentation, and further development. In this direction, the new millennium has seen an AAAISymposium (Spring 2001), a Dagstuhl seminar (in 2002), and the publication of the first textbook onthe topic (Baral, 2003). This special issues follows those events.
This note is about the relationship between two theories of negation as failure - one based on program completion, the other based on stable models, or answer sets. Francois Fages showed that if a logic program satisf...
详细信息
This note is about the relationship between two theories of negation as failure - one based on program completion, the other based on stable models, or answer sets. Francois Fages showed that if a logic program satisfies a certain syntactic condition, which is now called 'tightness,' then its stable models can be characterized as the models of its completion. We extend the definition of tightness and Fages' theorem to programs with nested expressions in the bodies of rules, and study tight logic programs containing the definition of the transitive closure of a predicate.
This paper describes the LDL++ system and the research advances that have enabled its design and development. We begin by discussing the new nonmonotonic and nondeterministic constructs that extend the functionality o...
详细信息
This paper describes the LDL++ system and the research advances that have enabled its design and development. We begin by discussing the new nonmonotonic and nondeterministic constructs that extend the functionality of the LDL++ language, while preserving its model-theoretic and fixpoint semantics. Then, we describe the execution model and the open architecture designed to support these new constructs and to facilitate the integration with existing DBMSs and applications. Finally, we describe the lessons learned by using LDL++ on various tested applications, such as middleware and datamning.
The proceedings contain 28 papers. The topics discussed include: outlier detection using default logic;translation of aggregate programs to normal logic programs;complexity of answer set checking and bounded predicate...
The proceedings contain 28 papers. The topics discussed include: outlier detection using default logic;translation of aggregate programs to normal logic programs;complexity of answer set checking and bounded predicate parities for non-ground answer set programming;parametric connectives in disjunctive logicprogramming;graphs and colorings for answer set programming: abridged report;eliminating disjunction from propositional logic programs under stable model preservation;a counter-based approach to translating normal logic programs into sets of clauses;integrating semantic web reasoning and answer set programming;using criticalities as a heuristic for answer set programming;implementing OCLP as a front-end for answer set solvers: from theory to practice;computing answer sets of a logic program via-enumeration of sat certificates;mappings between domain models in answer set programming;and towards the use of semantic contents in ASP for planning and diagnostic in GIS.
Most recently, Answer Set programming (ASP) has been attracting interest as a new paradigm for problem solving. An important aspect, for which several approaches have been presented, is the handling of preferences bet...
详细信息
Most recently, Answer Set programming (ASP) has been attracting interest as a new paradigm for problem solving. An important aspect, for which several approaches have been presented, is the handling of preferences between rules. In this paper, we consider the problem of implementing preference handling approaches by means of meta-interpreters in Answer Set programming. In particular, we consider the preferred answer set approaches by Brewka and Eiter, by Delgrande, Schaub and Tompits, and by Wang, Zhou and Lin. We present suitable meta-interpreters for these semantics using DLV, which is an efficient engine for ASP. Moreover, we also present a meta-interpreter for the weakly preferred answer set approach by Brewka and Eiter, which uses the weak constraint feature of DLV as a tool for expressing and solving an underlying optimization problem. We also consider advanced meta-interpreters, which make use of graph-based characterizations and often allow for more efficient computations. Our approach shows the suitability of ASP in general and of DLV in particular for fast prototyping. This can be fruitfully exploited for experimenting with new languages and knowledge-representation formalisms.
Ordered Choice logicprogramming (OCLP) allows for preference-based decision-making with multiple alternatives and without the burden of any form of negation. This complete absence of negation does not weaken the lang...
详细信息
Ordered Choice logicprogramming (OCLP) allows for preference-based decision-making with multiple alternatives and without the burden of any form of negation. This complete absence of negation does not weaken the language as both forms (classical and as-failure) can be intuitively simulated in the language. The semantics of the language is based on the preference between alternatives, yielding both a skeptical and a credulous approach. In this paper we discuss the theoretical basis for the implementation of an OCLP front-end for answer set solvers that can compute both semantics in an efficient manner. Both the basic algorithm and the proposed optimizations can be used in general and are not tailored towards any particular answer set solver.
The proceedings contain 27 papers. The special focus in this conference is on programming Languages and Systems. The topics include: Computer security from a programming language and static analysis perspective;the ev...
ISBN:
(纸本)3540008861
The proceedings contain 27 papers. The special focus in this conference is on programming Languages and Systems. The topics include: Computer security from a programming language and static analysis perspective;the evolution of requirements specification in formal cryptographic protocol analysis;a tail-recursive semantics for stack inspections;correction of functional logic programs;goal-independent suspension analysis for logic programs with dynamic scheduling;a simple language for real-time cryptographic protocol analysis;on the secure implementation of security protocols;handling encryption in an analysis for secure information flow;using controller synthesis to build property-enforcing layers;automatic software model checking using CLP;verifying temporal heap properties specified via evolution logic;correctness of data representations involving heap data structures;type error slicing in implicitly typed higher-order languages;requirements on the execution of Kahn process networks;building certified libraries for PCC;finite differencing of logical formulas for static analysis and register allocation by proof transformation.
A lambda-free logical framework takes parameterisation and definitions as the basic notions to provide schematic mechanisms for specification of type theories and their use in practice. The framework presented here, P...
详细信息
A lambda-free logical framework takes parameterisation and definitions as the basic notions to provide schematic mechanisms for specification of type theories and their use in practice. The framework presented here, PAL(+), is a logical framework for specification and implementation of type theories, such as Martin-Lof's type theory or UTT As in Martin-Lof's logical framework (Nordstrom et al., 1990), computational rules can be introduced and are used to give meanings to the declared constants. However, PAL(+) only allows one to talk about the concepts that are intuitively in the object type theories: types and their objects, and families of types and families of objects of types. In particular, in PAL(+), one cannot directly represent families of families of entities, which could be done in other logical frameworks by means of lambda abstraction. PAL(+) is in the spirit of de Bruijn's PAL for Automath (de Bruijn, 1986). Compared with PAL, PAL(+) allows one to represent parametric concepts such as families of types and families of non-parametric objects, which can be used by themselves as totalities as well as when they are fully instantiated. Such parametric objects are represented by local definitions (let-expressions). We claim that PAL(+) is a correct meta-language for specifying type theories (e.g., dependent type theories), as it has the advantage of exactly capturing the intuitive concepts in object type theories, and that its implementation reflects the actual use of type theories in practice. We shall study the meta-theory of PAL(+) by developing its typed operational semantics and showing that it has nice meta-theoretic properties.
An extension of constraint logicprogramming that allows for weighted partial satisfaction of soft constraints is described and applied to the development of an automated timetabling system for Purdue University. The ...
详细信息
ISBN:
(纸本)3540406999
An extension of constraint logicprogramming that allows for weighted partial satisfaction of soft constraints is described and applied to the development of an automated timetabling system for Purdue University. The soft-constraint solver implemented in the proposed solution approach allows constraint propagation for hard constraints together with preference propagation for soft constraints. A new repair search algorithm is proposed to improve upon initially generated (partial) assignments of the problem variables. The model and search methods applied to the solution of the large lecture room component are presented and discussed along with the computational results.
We present new complexity results on answer set checking for nonground programs under a variety of syntactic restrictions. For several of these problems, the kind of representation of the answer set to be checked is i...
详细信息
We present new complexity results on answer set checking for nonground programs under a variety of syntactic restrictions. For several of these problems, the kind of representation of the answer set to be checked is important. In particular, we consider set-based and bitmap-based representations, which are popular in implementations of Answer Set programming systems. Furthermore, we present new complexity results for various reasoning tasks under the assumption that predicate arities are bounded by some constant. These results imply that in such a setting - which appears to be a reasonable assumption in practice - more efficient implementations than those currently available may be feasible.
暂无评论