In this paper, a possibilistic disjunctive logicprogramming approach for modeling uncertain, incomplete, and inconsistent information is defined. This approach introduces the use of possibilistic disjunctive clauses,...
详细信息
In this paper, a possibilistic disjunctive logicprogramming approach for modeling uncertain, incomplete, and inconsistent information is defined. This approach introduces the use of possibilistic disjunctive clauses, which are able to capture incomplete information and states of a knowledge base at the same time. By considering a possibilistic logic program as a possibilistic logictheory, a construction of a possibilistic logicprogramming semantic based on answer sets and the proof theory of possibilistic logic is defined. It shows that this possibilistic semantics for disjunctive logic programs can be characterized by a fixed-point operator. It is also shown that the suggested possibilistic semantics can be computed by a resolution algorithm and the consideration of optimal refutations from a possibilistic logictheory. In order to manage inconsistent possibilistic logic programs, a preference criterion between inconsistent possibilistic models is defined. In addition, the approach of cuts for restoring consistency of an inconsistent possibilistic knowledge base is adopted. The approach is illustrated in a medical scenario.
Distribution semantics is one of the most prominent approaches for the combination of logicprogramming and probability theory. Many languages follow this semantics, such as Independent Choice logic, PRISM, pD, logic ...
详细信息
Distribution semantics is one of the most prominent approaches for the combination of logicprogramming and probability theory. Many languages follow this semantics, such as Independent Choice logic, PRISM, pD, logic Programs with Annotated Disjunctions (LPADs), and ProbLog. When a program contains functions symbols, the distribution semantics is well-defined only if the set of explanations for a query is finite and so is each explanation. Well-definedness is usually either explicitly imposed or is achieved by severely limiting the class of allowed programs. In this paper, we identify a larger class of programs for which the semantics is well-defined together with an efficient procedure for computing the probability of queries. Since logic Programs with Annotated Disjunctions offer the most general syntax, we present our results for them, but our results are applicable to all languages under the distribution semantics. We present the algorithm "Probabilistic Inference with Tabling and Answer subsumption" (PITA) that computes the probability of queries by transforming a probabilistic program into a normal program and then applying SLG resolution with answer subsumption. PITA has been implemented in XSB and tested on six domains: two with function symbols and four without. The execution times are compared with those of ProbLog, cplint, and CVE. PITA was almost always able to solve larger problems in a shorter time, on domains with and without function symbols.
This article is devoted to the study of methods to change defeasible logic programs (de.l.p.s) which are the knowledge bases used by the Defeasible logicprogramming (DeLP) interpreter. DeLP is an argumentation formal...
详细信息
This article is devoted to the study of methods to change defeasible logic programs (de.l.p.s) which are the knowledge bases used by the Defeasible logicprogramming (DeLP) interpreter. DeLP is an argumentation formalism that allows to reason over potentially inconsistent de.l.p.s. Argument theory Change (ATC) studies certain aspects of belief revision in order to make them suitable for abstract argumentation systems. In this article, abstract arguments are rendered concrete by using the particular rule-based defeasible logic adopted by DeLP. The objective of our proposal is to define prioritized argument revision operators a la ATC for de.l.p.s, in such a way that the newly inserted argument ends up undefeated after the revision, thus warranting its conclusion. In order to ensure this warrant, the de. l. p. has to be changed in concordance with a minimal change principle. To this end, we discuss different minimal change criteria that could be adopted. Finally, an algorithm is presented, implementing the argument revision operations.
We provide a method of translating theories of Nute's defeasible logic into logic programs, and a corresponding translation in the opposite direction. Under certain natural restrictions, the conclusions of defeasi...
详细信息
We provide a method of translating theories of Nute's defeasible logic into logic programs, and a corresponding translation in the opposite direction. Under certain natural restrictions, the conclusions of defeasible theories under the ambiguity propagating defeasible logic ADL correspond to those of the well-founded semantics for normal logic programs, and so it turns out that the two formalisms are closely related. Using the same translation of logic programs into defeasible theories, the semantics for the ambiguity blocking defeasible logic NDL can be seen as indirectly providing an ambiguity blocking semantics for logic programs. We also provide antimonotone operators for both ADL and NDL, each based on the Gelfond-Lifschitz (GL) operator for logic programs. For defeasible theories without defeaters or priorities on rules, the operator for ADL corresponds to the GL operator and so can be seen as partially capturing the consequences according to ADL. Similarly, the operator for NDL captures the consequences according to NDL, though in this case no restrictions on theories apply. Both operators can be used to define stable model semantics for defeasible theories.
Rewriting logic is an executable logical framework well suited for the semantic definition of languages. Any such framework has to be judged by its effectiveness to bridge the existing gap between language definitions...
详细信息
Rewriting logic is an executable logical framework well suited for the semantic definition of languages. Any such framework has to be judged by its effectiveness to bridge the existing gap between language definitions on the one hand, and language implementations and language analysis tools on the other. We give a progress report on how researchers in the rewriting logic semantics project are narrowing the gap between theory and practice in areas such as: modular semantic definitions of languages;scalability to real languages;support for real time;semantics of software and hardware modeling languages;and semantics-based analysis tools such as static analyzers, model checkers, and program provers. (C) 2013 Published by Elsevier Inc.
Fuzzy answer set programming (FASP) is a recent formalism for knowledge representation that enriches the declarativity of answer set programming by allowing propositions to be graded. To now, no implementations of FAS...
详细信息
Fuzzy answer set programming (FASP) is a recent formalism for knowledge representation that enriches the declarativity of answer set programming by allowing propositions to be graded. To now, no implementations of FASP solvers are available and all current proposals are based on compilations of logic programs into different paradigms, like mixed integer programs or bilevel programs. These approaches introduce many auxiliary variables which might affect the performance of a solver negatively. To limit this downside, operators for approximating fuzzy answer sets can be introduced: Given a FASP program, these operators compute lower and upper bounds for all atoms in the program such that all answer sets are between these bounds. This paper analyzes several operators of this kind which are based on linear programming, fuzzy unfounded sets and source pointers. Furthermore, the paper reports on a prototypical implementation, also describing strategies for avoiding computations of these operators when they are guaranteed to not improve current bounds. The operators and their implementation can be used to obtain more constrained mixed integer or bilevel programs, or even for providing a basis for implementing a native FASP solver. Interestingly, the semantics of relevant classes of programs with unique answer sets, like positive programs and programs with stratified negation, can be already computed by the prototype without the need for an external tool.
Recent years have witnessed an increasing interest in enhancing answer set solvers by allowing function symbols. Since the introduction of function symbols makes common inference tasks undecidable, research has focuse...
详细信息
Recent years have witnessed an increasing interest in enhancing answer set solvers by allowing function symbols. Since the introduction of function symbols makes common inference tasks undecidable, research has focused on identifying classes of programs allowing only a restricted use of function symbols while ensuring decidability of common inference tasks. Finitely-ground programs, introduced in Calimeri et al. (2008), are guaranteed to admit a finite number of stable models with each of them of finite size. Stable models of such programs can be computed and thus common inference tasks become decidable. Unfortunately, checking whether a program is finitely-ground is semi-decidable. This has led to several decidable criteria, called termination criteria, providing sufficient conditions for a program to be finitely-ground. This paper presents a new technique that, used in conjunction with current termination criteria, allows us to detect more programs as finitely-ground. Specifically, the proposed technique takes a logic program P and transforms it into an adorned program P-mu with the aim of applying termination criteria to P-mu rather than P. The transformation is sound in that if the adorned program satisfies a certain termination criterion, then the original program is finitely-ground. Importantly, applying termination criteria to adorned programs rather than the original ones strictly enlarges the class of programs recognized as finitely-ground.
In this paper, we combine Answer Set programming (ASP) with Dynamic Linear Time Temporal logic (DLTL) to define a temporal logicprogramming language for reasoning about complex actions and infinite computations. DLTL...
详细信息
In this paper, we combine Answer Set programming (ASP) with Dynamic Linear Time Temporal logic (DLTL) to define a temporal logicprogramming language for reasoning about complex actions and infinite computations. DLTL extends propositional temporal logic of linear time with regular programs of propositional dynamic logic, which are used for indexing temporal modalities. The action language allows general DLTL formulas to be included in domain descriptions to constrain the space of possible extensions. We introduce a notion of Temporal Answer Set for domain descriptions, based on the usual notion of Answer Set. Also, we provide a translation of domain descriptions into standard ASP and use Bounded Model Checking (BMC) techniques for the verification of DLTL constraints.
We present a new execution strategy for constraint logic programs called Failure Tabled CLP. Similarly to Tabled CLP our strategy records certain derivations in order to prune further derivations. However, our method ...
We present a new execution strategy for constraint logic programs called Failure Tabled CLP. Similarly to Tabled CLP our strategy records certain derivations in order to prune further derivations. However, our method only learns from failed derivations. This allows us to compute interpolants rather than constraint projection for generation of reuse conditions. As a result, our technique can be used where projection is too expensive or does not exist. Our experiments indicate that Failure Tabling can speed up the execution of programs with many redundant failed derivations as well as achieve termination in the presence of infinite executions.
The paper provides a framework for the verification of business processes, based on an extension of answer set programming (ASP) with temporal logic and constraints. The framework allows to capture expressive fluent a...
详细信息
The paper provides a framework for the verification of business processes, based on an extension of answer set programming (ASP) with temporal logic and constraints. The framework allows to capture expressive fluent annotations as well as data awareness in a uniform way. It allows for a declarative specification of a business process but also for encoding processes specified in conventional workflow languages. Verification of temporal properties of a business process, including verification of compliance to business rules, is performed by bounded model checking techniques in Answer Set programming, extended with constraint solving for dealing with conditions on numeric data.
暂无评论