We present a general logical framework for reasoning about agents' cognitive attitudes of both epistemic type and motivational type. We show that it allows us to express a variety of relevant concepts for qualitat...
详细信息
We present a general logical framework for reasoning about agents' cognitive attitudes of both epistemic type and motivational type. We show that it allows us to express a variety of relevant concepts for qualitative decision theory including the concepts of knowledge, belief, strong belief, conditional belief, desire, conditional desire, strong desire, and preference. We also present two extensions of the logic, one by the notion of choice and the other by dynamic operators for belief change and desire change, and we apply the former to the analysis of single-stage games under incomplete information. We provide sound and complete axiomatizations for the basic logic and for its two extensions.
We present a solution to real-world train scheduling problems, involving routing, scheduling, and optimization, based on Answer Set programming (ASP). To this end, we pursue a hybrid approach that extends ASP with dif...
详细信息
We present a solution to real-world train scheduling problems, involving routing, scheduling, and optimization, based on Answer Set programming (ASP). To this end, we pursue a hybrid approach that extends ASP with difference constraints to account for a fine-grained timing. More precisely, we exemplarily show how the hybrid ASP system clingo[DL] can be used to tackle demanding planning and scheduling problems. In particular, we investigate how to boost performance by combining distinct ASP solving techniques, such as approximations and heuristics, with preprocessing and encoding techniques for tackling large-scale, real-world train-scheduling instances.
This article is written in support of the academic discipline "Nonclassical logics". The objects of study within this discipline are the basic principles and constructive elements used in formal construction...
详细信息
This article is written in support of the academic discipline "Nonclassical logics". The objects of study within this discipline are the basic principles and constructive elements used in formal construction of various nonclassical propositional logics. Despite the abstract nature of the theory of nonclassical logics, which is mainly focused on strict mathematical formalization of logical reasoning, there are real practical applications for its theoretical results. In particular, languages of temporal modal logics are widely used for modeling, specification, and verification (correctness analysis) of logic control program systems. This article demonstrates, based on the example of linear temporal logic (LTL), how abstract concepts of nonclassical logics can be applied in practice in the area of information technology and programming. It is shown that the behavior of a software system can be represented as a set of LTL formulas, which can then be used to check the satisfiability of the properties of that software system via the procedure for proving the validity of logical inferences expressed in terms of linear temporal logic (LTL). The approach to using LTL to specify the behavior of software systems is demonstrated based on Minsky counter machines. Minsky machines are one of the ways of formalizing the intuitive concept of an algorithm. Their computational power is equivalent to that of Turing machines. A counter machine is a computer program written in a high-level language, since it contains variables called counters and conditional and unconditional jump operators used for loop construction. It is known that any algorithm can (hypothetically) be implemented as a three-counter Minsky machine.
Several AI problems can be conveniently modelled in ASP, and many of them require to enumerate solutions characterized by an optimality property that can be expressed in terms of subset-minimality with respect to some...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Several AI problems can be conveniently modelled in ASP, and many of them require to enumerate solutions characterized by an optimality property that can be expressed in terms of subset-minimality with respect to some objective atoms. In this context, solutions are often either (i) answer sets or (ii) sets of atoms that enforce the absence of answer sets on the ASP program at hand such sets are referred to as minimal unsatisfiable subsets (MUSes). In both cases, the required enumeration task is currently not supported by state-of-the-art ASP solvers.
Modal logic S5 has attracted significant attention and has led to several practical applications, owing to its simplified approach to dealing with nesting modal operators. Efficient implementations for evaluating sati...
详细信息
Modal logic S5 has attracted significant attention and has led to several practical applications, owing to its simplified approach to dealing with nesting modal operators. Efficient implementations for evaluating satisfiability of S5 formulas commonly rely on Skolemisation to convert them into propositional logic formulas, essentially by introducing copies of propositional atoms for each set of interpretations (possible worlds). This approach is simple, but often results into large formulas that are too difficult to process, and therefore more parsimonious constructions are required. In this work, we propose to use Answer Set programming for implementing such constructions, and in particular for identifying the propositional atoms that are relevant in every world by means of a reachability relation. The proposed encodings are designed to take advantage of other properties such as entailment relations of subformulas rooted by modal operators. An empirical assessment of the proposed encodings shows that the reachability relation is very effective and leads to comparable performance to a state-of-the-art S5 solver based on SAT, while entailment relations are possibly too expensive to reason about and may result in overhead.
Using answer set programming in real-world applications requires that the answer set program is correct and adequately represents knowledge. In this paper, we present strategies to resolve unintended contradictory sta...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Using answer set programming in real-world applications requires that the answer set program is correct and adequately represents knowledge. In this paper, we present strategies to resolve unintended contradictory statements resulting from modelling gaps and other flaws by modifying the program without manipulating the actual conflicting rules (inconsistency-causing rules with complementary head literals). We show how latent conflicts can be detected to prevent further conflicts during the resolution process or after subsequent modifications in the future. The presented approach is another step towards a general framework where professional experts who are not necessarily familiar with ASP can repair existing answer set programs and independently resolve conflicts resulting from contradictory statements in an informative way. In such a framework, conflict resolution strategies allow for generating possible solutions that consist of informative extensions and modifications of the program. In interaction with the professional expert, these solution options can then be used to obtain the solution that represents the underlying knowledge best.
We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on constrained Horn clauses (CHCs) by which the verification probl...
详细信息
We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on constrained Horn clauses (CHCs) by which the verification problem is reduced to the problem of checking satisfiability of a set of clauses derived from the given program and contracts. We consider programs that manipulate algebraic data types (ADTs) and a class of contracts specified by catamorphisms, that is, functions defined by simple recursion schemata on the given ADTs. We show by several examples that state-of-the-art CHC satisfiability tools are not effective at solving the satisfiability problems obtained by direct translation of the contracts into CHCs. To overcome this difficulty, we propose a transformation technique that removes the ADT terms from CHCs and derives new sets of clauses that work on basic sorts only, such as integers and booleans. Thus, when using the derived CHCs there is no need for induction rules on ADTs. We prove that the transformation is sound, that is, if the derived set of CHCs is satisfiable, then so is the original set. We also prove that the transformation always terminates for the class of contracts specified by catamorphisms. Finally, we present the experimental results obtained by an implementation of our technique when verifying many non-trivial contracts for ADT manipulating programs.
Both logicprogramming in general and Prolog in particular have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A large body of research has been gathered o...
详细信息
Both logicprogramming in general and Prolog in particular have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A large body of research has been gathered over the last 50 years, supported by many Prolog implementations. Many implementations are still actively developed, while new ones keep appearing. Often, the features added by different systems were motivated by the interdisciplinary needs of programmers and implementors, yielding systems that, while sharing the "classic" core language, in particular, the main aspects of the ISO-Prolog standard, also depart from each other in other aspects. This obviously poses challenges for code portability. The field has also inspired many related, but quite different languages that have created their own communities. This article aims at integrating and applying the main lessons learned in the process of evolution of Prolog. It is structured into three major parts. First, we overview the evolution of Prolog systems and the community approximately up to the ISO standard, considering both the main historic developments and the motivations behind several Prolog implementations, as well as other logicprogramming languages influenced by Prolog. Then, we discuss the Prolog implementations that are most active after the appearance of the standard: their visions, goals, commonalities, and incompatibilities. Finally, we perform a SWOT analysis in order to better identify the potential of Prolog and propose future directions along with which Prolog might continue to add useful features, interfaces, libraries, and tools, while at the same time improving compatibility between implementations.
Extending the popular answer set programming paradigm by introspective reasoning capacities has received increasing interest within the last years. Particular attention is given to the formalism of epistemic logic pro...
详细信息
Extending the popular answer set programming paradigm by introspective reasoning capacities has received increasing interest within the last years. Particular attention is given to the formalism of epistemic logic programs (ELPs) where standard rules are equipped with modal operators which allow to express conditions on literals for being known or possible, that is, contained in all or some answer sets, respectively. ELPs thus deliver multiple collections of answer sets, known as world views. Employing ELPs for reasoning problems so far has mainly been restricted to standard decision problems (complexity analysis) and enumeration (development of systems) of world views. In this paper, we take a next step and contribute to epistemic logicprogramming in two ways: First, we establish quantitative reasoning for ELPs, where the acceptance of a certain set of literals depends on the number (proportion) of world views that are compatible with the set. Second, we present a novel system that is capable of efficiently solving the underlying counting problems required to answer such quantitative reasoning problems. Our system exploits the graph-based measure treewidth and works by iteratively finding and refining (graph) abstractions of an ELP program. On top of these abstractions, we apply dynamic programming that is combined with utilizing existing search-based solvers like (e)clingo for hard combinatorial subproblems that appear during solving. It turns out that our approach is competitive with existing systems that were introduced recently.
Existential rules are a positive fragment of first-order logic that generalizes function-free Horn rules by allowing existentially quantified variables in rule heads. This family of languages has recently attracted si...
详细信息
Existential rules are a positive fragment of first-order logic that generalizes function-free Horn rules by allowing existentially quantified variables in rule heads. This family of languages has recently attracted significant interest in the context of ontology-mediated query answering. Forward chaining, also known as the chase, is a fundamental tool for computing universal models of knowledge bases, which consist of existential rules and facts. Several chase variants have been defined, which differ on the way they handle redundancies. A set of existential rules is bounded if it ensures the existence of a bound on the depth of the chase, independently from any set of facts. Deciding if a set of rules is bounded is an undecidable problem for all chase variants. Nevertheless, when computing universal models, knowing that a set of rules is bounded for some chase variant does not help much in practice if the bound remains unknown or even very large. Hence, we investigate the decidability of the k-boundedness problem, which asks whether the depth of the chase for a given set of rules is bounded by an integer k. We identify a general property which, when satisfied by a chase variant, leads to the decidability of k-boundedness. We then show that the main chase variants satisfy this property, namely the oblivious, semi-oblivious (aka Skolem), and restricted chase, as well as their breadth-first versions.
暂无评论