We have studied the update operator circle plus(1) defined for update sequences by Eiter et al. without tautologies and we have observed that it satisfies an interesting property(1). This property, which we call Weak ...
详细信息
We have studied the update operator circle plus(1) defined for update sequences by Eiter et al. without tautologies and we have observed that it satisfies an interesting property(1). This property, which we call Weak Independence of Syntax (WIS), is similar to one of the postulates proposed by Alchourron, Gardenfors, and Makinson (AGM);only that in this case it applies to nonmonotonic logic. In addition, we consider other five additional basic properties about update programs and we show that circle plus(1) satisfies them. This work continues the analysis of the AGM postulates with respect to the circle plus(1) operator under a refined view that considers N-2 as a monotonic logic which allows us to expand our understanding of answer sets. Moreover, N-2 helped us to derive an alternative definition of circle plus(1) avoiding the use of unnecessary extra atoms.
This technical note describes a monotone and continuous fixpoint operator to compute the answer sets of programs with aggregates. The fixpoint operator relies on the notion of aggregate solution. Under certain conditi...
详细信息
This technical note describes a monotone and continuous fixpoint operator to compute the answer sets of programs with aggregates. The fixpoint operator relies on the notion of aggregate solution. Under certain conditions, this operator behaves identically to the three-valued immediate consequence operator Phi(aggr)(P) for aggregate programs, independently proposed in Pelov (2004) and Pelov et al. (2004). This operator allows us to closely tie the computational complexity of the answer set checking and answer sets existence problems to the cost of checking a solution of the aggregates in the program. Finally, we relate the semantics described by the operator to other proposals for logicprogramming with aggregates.
In answer set programming (ASP), a problem at hand is solved by (i) writing a logic program whose answer sets correspond to the solutions of the problem, and by (ii) computing the answer sets of the program using an a...
详细信息
In answer set programming (ASP), a problem at hand is solved by (i) writing a logic program whose answer sets correspond to the solutions of the problem, and by (ii) computing the answer sets of the program using an answer set solver as a search engine. Typically, a programmer creates a series of gradually improving logic programs for a particular problem when optimizing program length and execution time on a particular solver. This leads the programmer to a meta-level problem of ensuring that the programs are equivalent, i.e., they give rise to the same answer sets. To case answer set programming at methodological level, we propose a translation-based method for verifying the equivalence of logic programs. The basic idea is to translate logic programs P and Q under consideration into a single logic program EQT(P,Q) whose answer sets (if such exist) yield counter-examples to the equivalence of P and Q. The method is developed here in a slightly more general setting by taking the visibility of atoms properly into account when comparing answer sets. The translation-based approach presented in the paper has been implemented as a translator called LPEQ that enables the verification of weak equivalence within the SMODELS system using the same search engine as for the search of models. Our experiments with LPEQ and SMODELS suggest that establishing the equivalence of logic programs in this way is in certain cases much faster than naive cross-checking of answer sets.
Meseguer's rewriting logic and the rewriting logic CRWL are two well-known approaches to rewriting as logical deduction that, despite some clear similarities, were designed with different objectives. Here we study...
详细信息
Meseguer's rewriting logic and the rewriting logic CRWL are two well-known approaches to rewriting as logical deduction that, despite some clear similarities, were designed with different objectives. Here we study the relationships between them, both at a syntactic and at a semantic level. Even though it is not possible to establish an entailment system map between them, both can be naturally simulated in each other. Semantically, there is no embedding between the corresponding institutions. Along the way, the notions of entailment and satisfaction in Meseguer's rewriting logic are generalized.
In this paper we present the theory and practice of co-logicprogramming (co-LP for brevity), a paradigm that combines both inductive and coinductive logicprogramming. Co-LP is a natural generalization of logic progr...
详细信息
ISBN:
(纸本)9783540734192
In this paper we present the theory and practice of co-logicprogramming (co-LP for brevity), a paradigm that combines both inductive and coinductive logicprogramming. Co-LP is a natural generalization of logicprogramming and coinductive logicprogramming, which in turn generalizes other extensions of logicprogramming, such as infinite trees, lazy predicates, and concurrent communicating predicates. Co-LP has applications to rational trees, verifying infinitary properties, lazy evaluation, concurrent LP, model checking, bisimilarity proofs, etc.
The design and implementation of an incremental copying heap garbage collector for WAM-based Prolog systems is presented. Its heap layout consists of a number of equal-sized blocks. Other changes to the standard WAM a...
详细信息
Through the Internet and the World-Wide Web, a vast number of information sources has become available, which offer information on various subjects by different providers, often in heterogeneous formats. This calls fo...
详细信息
Through the Internet and the World-Wide Web, a vast number of information sources has become available, which offer information on various subjects by different providers, often in heterogeneous formats. This calls for tools and methods for building an advanced information-processing infrastructure. One issue in this area is the selection of suitable information sources in query answering. In this paper, we present a knowledge-based approach to this problem, in the setting where one among a set of information sources (prototypically, data repositories) should be selected for evaluating a user query. We use extended logic programs (ELPs) to represent rich descriptions of the information sources, an underlying domain theory, and user queries in a formal query language (here, XML-QL, but other languages can be handled as well). Moreover, we use ELPs for declarative query analysis and generation of a query description. Central to our approach are declarative source-selection programs, for which we define syntax and semantics. Due to the structured nature of the considered data items, the semantics of such programs must carefully respect implicit context information in source-selection rules, and furthermore combine it with possible user preferences. A prototype implementation of our approach has been realized exploiting the DLV KR system and its plp front-end for prioritized ELPs. We describe a representative example involving specific movie databases, and report about experimental results.
In this paper, we present a new approach, called NM-ILP-IP, for inductive learning in the context of nonmonotonic logic frameworks. This approach is based on the notations of concept instances and instance patterns in...
详细信息
It is common practice in both theoretical computer science and theoretical physics to describe the (static) logic of a system by means of a complete lattice. When formalizing the dynamics of such a system, the updates...
详细信息
It is common practice in both theoretical computer science and theoretical physics to describe the (static) logic of a system by means of a complete lattice. When formalizing the dynamics of such a system, the updates of that system organize themselves quite naturally in a quantale, or more generally, a quantaloid. In fact, we are led to consider cocomplete quantaloid-enriched categories as a fundamental mathematical structure for a dynamic logic common to both computer science and physics. Here we explain the theory of totally continuous cocomplete categories as a generalization of the well-known theory of totally continuous suplattices. That is to say, we undertake some first steps towards a theory of "dynamic domains". (c) 2007 Elsevier B.V. All rights reserved.
暂无评论