Model-based Diagnosis (MBD) is an approach to diagnosis, where an (objective) model of a system is diagnosed to find a set of explanations revealing root causes for issues. Temporal behavioral models are prominent app...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Model-based Diagnosis (MBD) is an approach to diagnosis, where an (objective) model of a system is diagnosed to find a set of explanations revealing root causes for issues. Temporal behavioral models are prominent approach for temporal MBD, where their associated temporal formulas (TBFs) by Brusoni et al. (Artificial Intelligence, 102:39-79, 1998) can be used to relate explanations to observations under temporal constraints based on Allen's Interval Algebra (IA). Due to expressive limitations of the constructs, we envision an extended language of TBFs that allows for complex formulas and nesting of formulas in temporal constraints. To this end, we present a language that extends propositional resp. FO logic with IA relations and provide semantics for it based on here-and-there (HT) logic as well as on Equilibrium logic. Furthermore, we lift a well-known tableau calculus for propositional HT logic to the temporal setting and report about an experimental prototype implementation. Based on these results, rich notions of diagnostic explanations from temporal behavior models may be developed.
We present a general approach to planning with incomplete information in Answer Set programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptio...
详细信息
We present a general approach to planning with incomplete information in Answer Set programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent planning problems using a simple formalism where logic programs describe the transition function between states, the initial states and the goal states. For solving planning problems, we use Quantified Answer Set programming (QASP), an extension of ASP with existential and universal quantifiers over atoms that is analogous to Quantified Boolean Formulas (QBFs). We define the language of quantified logic programs and use it to represent the solutions different variants of conformant and conditional planning. On the practical side, we present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver, and we evaluate experimentally the approach on conformant and conditional planning benchmarks.
Modal logic S5 is used extensively for representing knowledge that includes statements about necessity and possibility, owing to its simplicity in handling chained modal operators. Significant research effort has been...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Modal logic S5 is used extensively for representing knowledge that includes statements about necessity and possibility, owing to its simplicity in handling chained modal operators. Significant research effort has been devoted in developing efficient reasoning mechanisms over complex S5 formulas, resulting in various solvers taking advantage of the boolean satisfiability problem (SAT). Among them, the most performant solver implements a heuristic for identifying worlds that can be merged, hence reducing the size of SAT instances to be checked. Recently, Answer Set programming (ASP) has also been considered, and different ASP encodings were proposed and tested, reaching state-of-the-art performance. In particular, a heuristic for identifying the propositional atoms that are relevant in every world resulted in a performance gain in previous experiments. This work addresses the open question of whether the aforementioned two heuristics can be combined, as well as possibly enabling lazy instantiation of the resulting encodings, and what their potential impact is on the performance of the ASP-based solver. Experiments show that lazy creation of worlds provides some further performance gain to the ASP-based solver on the tested instances.
In temporal extensions of Answer Set programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts aw...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
In temporal extensions of Answer Set programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. In many applications, however, timing constraints are important like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in Metric Equilibrium logic and Monadic Quantified Equilibrium logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.
logic programs (LPs) and argumentation frameworks (AFs) are two declarative knowledge representation (KR) formalisms used for different reasoning tasks. The purpose of this study is interlinking two different reasonin...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
logic programs (LPs) and argumentation frameworks (AFs) are two declarative knowledge representation (KR) formalisms used for different reasoning tasks. The purpose of this study is interlinking two different reasoning components. To this end, we introduce two frameworks: LPAF and AFLP. The former enables to use the result of argumentation in AF for reasoning in LP, while the latter enables to use the result of reasoning in LP for arguing in AF. These frameworks are extended to bidirectional frameworks in which AF and LP can exchange information with each other. We also investigate their connection to several general KR frameworks from the literature.
Assumption-based argumentation (ABA) is a central structured argumentation formalism. As shown recently, answer set programming (ASP) enables efficiently solving NP-hard reasoning tasks of ABA in practice, in particul...
详细信息
Assumption-based argumentation (ABA) is a central structured argumentation formalism. As shown recently, answer set programming (ASP) enables efficiently solving NP-hard reasoning tasks of ABA in practice, in particular in the commonly studied logicprogramming fragment of ABA. In this work, we harness recent advances in incremental ASP solving for developing effective algorithms for reasoning tasks in the logicprogramming fragment of ABA that are presumably hard for the second level of the polynomial hierarchy, including skeptical reasoning under preferred semantics as well as preferential reasoning. In particular, we develop non-trivial counterexample-guided abstraction refinement procedures based on incremental ASP solving for these tasks. We also show empirically that the procedures are significantly more effective than previously proposed algorithms for the tasks.
We study the relationship between two approaches to higher-order program verification: a semi-automated method using Dijkstra monads and a fully automated method using a higher-order fixpoint logic called HFL(Z). Alth...
详细信息
In this paper, we present a syntactic transformation, called the unfolding operator, that allows forgetting an atom in a logic program (under ASP semantics). The main advantage of unfolding is that, unlike other synta...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
In this paper, we present a syntactic transformation, called the unfolding operator, that allows forgetting an atom in a logic program (under ASP semantics). The main advantage of unfolding is that, unlike other syntactic operators, it is always applicable and guarantees strong persistence, that is, the result preserves the same stable models with respect to any context where the forgotten atom does not occur. The price for its completeness is that the result is an expression that may contain the fork operator. Yet, we illustrate how, in some cases, the application of fork properties may allow us to reduce the fork to a logic program, even in conditions that could not be treated before using the syntactic methods in the literature.
Reasoning on defeasible knowledge is a topic of interest in the area of description logics, as it is related to the need of representing exceptional instances in knowledge bases. In this direction, in our previous wor...
详细信息
Reasoning on defeasible knowledge is a topic of interest in the area of description logics, as it is related to the need of representing exceptional instances in knowledge bases. In this direction, in our previous works we presented a framework for representing (contextualized) OWL RL knowledge bases with a notion of justified exceptions on defeasible axioms: reasoning in such framework is realized by a translation into ASP programs. The resulting reasoning process for OWL RL, however, introduces a complex encoding in order to capture reasoning on the negative information needed for reasoning on exceptions. In this paper, we apply the justified exception approach to knowledge bases in DL-Lite(R), that is, the language underlying OWL QL. We provide a definition for DL-Lite(R )knowledge bases with defeasible axioms and study their semantic and computational properties. In particular, we study the effects of exceptions over unnamed individuals. The limited form of DL-Lite(R) axioms allows us to formulate a simpler ASP encoding, where reasoning on negative information is managed by direct rules. The resulting materialization method gives rise to a complete reasoning procedure for instance checking in DL-LiteR with defeasible axioms.(1)
This paper introduces techniques to integrate WordNet into a Fuzzy logicprogramming system. Since WordNet relates words but does not give graded information on the relation between them, we have implemented standard ...
详细信息
This paper introduces techniques to integrate WordNet into a Fuzzy logicprogramming system. Since WordNet relates words but does not give graded information on the relation between them, we have implemented standard similarity measures and new directives allowing the proximity equations linking two words to be generated with an approximation degree. Proximity equations are the key syntactic structures which, in addition to a weak unification algorithm, make a flexible query-answering process possible in this kind of programming language. This addition widens the scope of Fuzzy logicprogramming, allowing certain forms of lexical reasoning, and reinforcing Natural Language Processing (NLP) applications.
暂无评论