We present a unifying approach to the efficient evaluation of propositional answer-set programs. Our approach is based on backdoors which are small sets of atoms that represent "clever reasoning shortcuts" t...
详细信息
ISBN:
(纸本)9781577355120
We present a unifying approach to the efficient evaluation of propositional answer-set programs. Our approach is based on backdoors which are small sets of atoms that represent "clever reasoning shortcuts" through the search space. The concept of backdoors is widely used in the areas of propositional satisfiability and constraint satisfaction. We show how this concept can be adapted to the nonmonotonic setting and how it allows to augment various known tractable subproblems, such as the evaluation of Horn and acyclic programs. In order to use backdoors we need to find them first. We utilize recent advances in fixed-parameter algorithmics to detect small backdoors. This implies fixed-parameter tractability of the evaluation of propositional answer-set programs, parameterized by the size of backdoors. Hence backdoor size provides a structural parameter similar to the treewidth parameter previously considered. We show that backdoor size and treewidth are incomparable, hence there are instances that are hard for one and easy for the other parameter. We complement our theoretical results with first empirical results.
In this proposal, we introduce Bayesian Abductive logic Programs (BALP), a probabilistic logic that adapts Bayesian logic Programs (BLPs) for abductive reasoning. Like BLPs, BALPs also combine first-order logic and Ba...
详细信息
ISBN:
(纸本)9781577355120
In this proposal, we introduce Bayesian Abductive logic Programs (BALP), a probabilistic logic that adapts Bayesian logic Programs (BLPs) for abductive reasoning. Like BLPs, BALPs also combine first-order logic and Bayes nets. However, unlike BLPs, which use deduction to construct Bayes nets, BALPs employ logical abduction. As a result, BALPs are more suited for problems like plan/activity recognition that require abductive reasoning. In order to demonstrate the efficacy of BALPs, we apply it to two abductive reasoning tasks - plan recognition and natural language understanding.
In this paper, we study algorithms for probabilistic satisfiability (PSAT), an NP-complete problem, and their empiric complexity distribution. We define a PSAT normal form, based on which we propose two logic-based al...
详细信息
ISBN:
(纸本)9781577355120
In this paper, we study algorithms for probabilistic satisfiability (PSAT), an NP-complete problem, and their empiric complexity distribution. We define a PSAT normal form, based on which we propose two logic-based algorithms: a reduction of normal form PSAT instances to SAT, and a linearalgebraic algorithmwith a logic-based column generation strategy. We conclude that both algorithms present a phase transition behaviour and that the latter has a much better performance.
It is well-known that satisfiability (and hence validity) in the minimal classical modal logic is a PSPACE-complete problem. In this paper we consider the satisfiability and validity problems (here they are not dual, ...
详细信息
ISBN:
(纸本)9781577355120
It is well-known that satisfiability (and hence validity) in the minimal classical modal logic is a PSPACE-complete problem. In this paper we consider the satisfiability and validity problems (here they are not dual, although mutually reducible) for the minimal modal logic over a finite Lukasiewicz chain, and show that they also are PSPACE-complete. This result is also true when adding either the Delta operator or truth constants in the language, i.e. in all these cases it is PSPACE-complete.
In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly i...
详细信息
ISBN:
(纸本)9781577355120
In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly increasing the number of forced propositional variables after the application of non-invertible rules. The focus of the paper is on a new tableau system for Dummett logic, for which we have an implementation.
We propose a logical framework to represent and reason about agent interactions in normative systems. Our starting point is a dynamic logic of propositional assignments whose satisfiability problem is PSPACE-complete....
详细信息
ISBN:
(纸本)9781577355120
We propose a logical framework to represent and reason about agent interactions in normative systems. Our starting point is a dynamic logic of propositional assignments whose satisfiability problem is PSPACE-complete. We show that it embeds Coalition logic of Propositional Control CL-PC and that various notions of ability and capability can be captured in it. We illustrate it on a water resource management case study. Finally, we show how the logic can be easily extended in order to represent constitutive rules which are also an essential component of the modelling of social reality.
Many AI applications are based on some underlying logic that tolerates inconsistent information in a non-trivial way. However, it is not always clear what should be the exact nature of such a logic, and how to choose ...
详细信息
ISBN:
(纸本)9781577355120
Many AI applications are based on some underlying logic that tolerates inconsistent information in a non-trivial way. However, it is not always clear what should be the exact nature of such a logic, and how to choose one for a specific application. In this paper, we formulate a list of desirable properties of "ideal" logics for reasoning with inconsistency, identify a variety of logics that have these properties, and provide a systematic way of constructing, for every n > 2, a family of such n-valued logics.
This paper presents a hardware-supported resource management methodology for massively parallel processor arrays. It enables processing elements to autonomously explore resource availability in their neighborhood. To ...
详细信息
ISBN:
(纸本)9781457712920
This paper presents a hardware-supported resource management methodology for massively parallel processor arrays. It enables processing elements to autonomously explore resource availability in their neighborhood. To support resource exploration, we introduce specialized controllers, which can be attached to each of the processing elements. We propose different types of architectures for the exploration controller: fast FSM-based designs as well as flexible programmable controllers. These controllers allow to implement different distributed resource exploration strategies in order to enable parallel programs the exploration and reservation of available resources according to different application requirements. Hardware cost evaluations show that the cost of the simplest implementation of our programmable controller is comparable to our FSM-based implementations, while offering the flexibility for implementing different exploration strategies. We show that the proposed distributed approach can achieve a significant speedup in comparison with centralized resource exploration methods.
We characterize the expressive power of description logic (DL) TBoxes, both for expressive DLs such as ALC and ALCQIO and lightweight DLs such as DL-Lite and EL. Our characterizations are relative to first-order logic...
详细信息
ISBN:
(纸本)9781577355120
We characterize the expressive power of description logic (DL) TBoxes, both for expressive DLs such as ALC and ALCQIO and lightweight DLs such as DL-Lite and EL. Our characterizations are relative to first-order logic, based on a wide range of semantic notions such as bisimulation, equisimulation, disjoint union, and direct product. We exemplify the use of the characterizations by a first study of the following novel family of decision problems: given a TBox T formulated in a DL L, decide whether T can be equivalently rewritten as a TBox in the fragment L′ of L.
Model checking is one of the most effective techniques in automated system verification. Although this technique can handle complex verifications, model checking tools usually do not give any suggestions on how to rep...
详细信息
ISBN:
(纸本)9781577355120
Model checking is one of the most effective techniques in automated system verification. Although this technique can handle complex verifications, model checking tools usually do not give any suggestions on how to repair inconsistent system models. In this paper, we show that approaches developed to update models of Computation Tree logic (CTL) cannot deal with all kinds of changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context.
暂无评论