Attribut:Abstract
Aus International Center for Computational Logic
Dies ist eine Eigenschaft des Typs Text.
"
Linear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that sigma is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and briefly discuss how the undecidability results transfer to first-order logic on words. +
(
ℰℒ is a popular description logic, used as a core formalism in large existing knowledge bases. Uniform interpolants of knowledge bases are of high interest, e.g. in scenarios where a knowledge base is supposed to be partially reused. However, to the best of our knowledge no procedure has yet been proposed that computes uniform ℰℒ interpolants of general ℰℒ terminologies. Up to now, also the bound on the size of uniform ℰℒ interpolants has remained unknown. In this article, we propose an approach to computing a finite uniform interpolant for a general ℰℒ terminology if it exists. To this end, we develop a quadratic representation of ℰℒ TBoxes as regular tree grammars. Further, we show that, if a finite uniform ℰℒ interpolant exists, then there exists one that is at most triple exponential in the size of the original TBox, and that, in the worst case, no smaller interpolants exist, thereby establishing tight worst-case bounds on their size. Beyond showing these bounds, the notions and results established in this paper also provide useful insights for designing efficient ontology reformulation algorithms, for instance, within the context of module extraction. +
1
11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning LPAR 2004 +
This volume contains the papers presented at the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), held from March 14 to 18, 2005, in Montevideo, Uruguay, together with the 5th International Workshop on the Implementation of Logics (organised by Stephan Schulz and Boris Konev) and the Workshop on Analytic Proof Systems (organised by Matthias Baaz). +
This volume contains the papers presented at the 18th International Conference on Rewriting Techniques and Applications (RTA'07), which was held on June 26--28, 2007, on the Paris campus of the Conservatoire National des Arts et Metiers (CNAM) in Paris, France. +
2
In 1984, Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidable in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004, the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime, thus 2-ExpTime-complete. We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted on tree structures. +
A
We propose a description-logic style extension of OWL 2 with nominal schemas which can be used like "variable nominal classes" within axioms. This feature allows ontology languages to express arbitrary DL-safe rules (as expressible in SWRL or RIF) in their native syntax. We show that adding nominal schemas to OWL 2 does not increase the worst-case reasoning complexity, and we identify a novel tractable language SROELV3(∩, x) that is versatile enough to capture the lightweight languages OWL EL and OWL RL. +
This introductory chapter to Conceptual Structures in Practice gives a quick overview of formal concept analysis (FCA) to provide necessary prerequisites for understanding the applied chapters later in the book. Besides essential notions like formal context, formal concept, and concept lattice, the chapter also specifically focusses on the aspect of (logic-based) knowledge representation in FCA, leading to the logic of attributes and to the important method of attribute exploration that is also applied in later chapters. +
We enrich the concept of automata with storage by weights taken from any unital valuation monoid. We prove a Chomsky-Schützenberger theorem for the class of weighted languages recognizable by such weighted automata with storage. +
Translations to (first-order) Datalog have been used in a number of inferencing techniques for description logics (DLs), yet the relationship between the semantic expressivities of function-free Horn logic and DL is understood only poorly. Although Description Logic Programs (DLP) have been described as DLs in the "expressive intersection" of DL and Datalog, it is unclear what an intersection of two syntactically incomparable logics is, even if both have a first-order logic semantics. In this work, we offer a characterisation for DL fragments that can be expressed, in a concrete sense, in Datalog. We then determine the largest such fragment for the DL ALC, and provide an outlook on the extension of our methods to more expressive DLs. +
A Comprehensive Analysis of the cf2 Argumentation Semantics: From Characterization to Implementation +
Argumentation is one of the major fields in Artificial Intelligence (AI). Numerous applications in diverse domains like legal reasoning, multi-agent systems, social networks, e-government, decision support and many more make this topic very interdisciplinary and lead to a wide range of different formalizations. Out of them the concept of abstract Argumentation Frameworks (AFs) is one of the most popular approaches to capture certain aspects of argumentation. This very simple yet expressive model has been introduced by Phan Minh Dung in 1995. Arguments and a binary attack relation between them, denoting conflicts, are the only components one needs for the representation of a wide range of problems and the reasoning therein.
Nowadays numerous semantics exist to solve the inherent conflicts between the arguments by selecting sets of “acceptable” arguments. Depending on the application, acceptability is defined in different ways. Some semantics are based on the idea to defend arguments against attacks, while others treat arguments like different choices and the solutions stand for consistent sets of arguments. A systematic analysis of these semantics on a theoretical and practical level is indispensable for the development of competitive systems. This includes a complete complexity analysis to develop appropriate algorithms and systems, the verification of the behavior on concrete instances as well as the identification of possible redundancies for specific semantics to simplify the frameworks.
In this thesis we exemplify such an analysis on the cf2 semantics which does not require to defend arguments against attacks but is based on a decomposition of the framework along its strongly connected components (SCCs). This allows to treat cycles in a more sensitive way than others and to overcome some problems which arise with odd- and even-length cycles. Due to the quite complicated definition of this semantics it has not been studied very intensively.
To facilitate further investigation steps we first introduce an alternative characterization of the cf2 semantics. Then we propose a small modification of this semantics to overcome a particular problematic behavior on specific instances which results in the sibling semantics stage2 . After a complete complexity analysis and the investigation of equivalences for these two semantics, we apply the obtained results on two different implementation methods, namely the reduction-based approach of answer-set programming and the direct implementation in terms of labeling-based algorithms.
Psychological experiments on syllogistic reasoning have shown that participants did not always deduce the classical logically valid conclusions.
In particular, the results show that they had difficulties to reason with syllogistic statements that contradicted their own beliefs. This paper discusses syllogisms in human reasoning and proposes a formalization under the weak completion semantics. +
Previous results have shown that weak completion semantics based on three-valued Łukasiewicz logic can adequately represent and explain human behavior in the suppression task. This approach corresponds to well-founded semantics for tight logic programs. In this paper we apply both semantics to the selection task – probably the most famous and best investigated psychological study about human reasoning with conditionals. In its abstract version, cards are shown to some people and they have to check if a conditional statement about the cards holds true. Numerous psychological studies show that most people do not solve this task correctly in terms of classical propositional logic and tend to make similar reasoning errors. Once the same reasoning problem is framed within a social setting, most people solve the task correctly. By distinguishing between belief and social constraints, we apply the abstract and the social case within the weak completion and the well-founded semantics and show that when reasoning towards the corresponding representations, our computational approach adequately reflects the psychological results.
Finally, we present a psychological study testing different predictions of the weak completion and the well-founded semantics on programs which are not tight. +
The tendency to accept or reject arguments based on own beliefs or prior knowledge rather than on the reasoning process is called the belief-bias effect. A psychological syllogistic reasoning task shows this phenomenon, wherein participants were asked whether they accept or reject a given syllogism. We discuss one case which is commonly assumed to be believable but not logically valid. By introducing abnormalities, abduction
and background knowledge, we model this case under the weak completion semantics. Our formalization reveals new questions about observations and their explanations which might include some relevant prior abductive contextual information concerning some side-effect. Inspection points, introduced by Pereira and Pinto, allow us to express these definitions syntactically and intertwine them into an operational semantics. +
A novel approach to human conditional reasoning based on the three-valued Łukasiewicz logic is presented. We will demonstrate that the Łukasiewicz logic overcomes problems the so far proposed Fitting logic has in reasoning with the suppression task. While adequately solving the suppression task, the approach gives rise to a number of open questions concerning the use of Łukasiewicz logic, unique fixed points, completion
versus weak completion, explanations, negation, and sceptical versus credulous approaches in human reasoning. +
Motivated by applications that demand for the adequate representation of part-whole relations, different possibilities of representing transitive relations in terminological knowledge representation systems are investigated. A well-known concept language, ALC, is extended by three different kinds of transitive roles. It turns out that these extensions differ largely in expressiveness and computational complexity, hence this investigation gives insight into the diverse alternatives for the representation of transitive relations such as part-whole relations, family relations or partial orders in general. +
We investigate how terminological knowledge representation systems can be used to support modeling in an engeneering application. Because of the high complexity of the application, support of top--down modeling is a quite ambitious, but useful task for TKR Systems. An interesting problem to solve in this context is the handling of composite objects. Therefor, not only different part-whole relations have to be represented (some of them are transitive) but also their transitivity-like interaction as well as local properties of these relations. Hence this application calls for a concept language with powerful role forming operators.
A concept language P with the expressive power to represent part-whole relations is defined, but it turns out that satisfiability of concept terms in P is undecidable. Hence it is necessary to drop some (but not many) of the demands made for the benefit of decidability. Several ways to handle the high complexity of inference algorithms of P are discussed. +
Description Logics (DLs) are formalisms for representing and reasoning about conceptual knowledge. There exist several extensions of DLs for an appropriate integration of temporal knowledge. This paper investigates the relation between the two DLs TL-ALCF and ALCF(D). TL-ALCF is an interval-based, temporal DL for reasoning about objects whose properties vary over time. ALCF(D) is a logic for integrated reasoning about conceptual and so-called concrete knowledge. If instantiated with a ``temporal'' concrete domain, ALCF(D) is well-suited for reasoning about temporal objects, i.e., objects which have a unique temporal extension. This paper is a first attempt to clarify the relationship between this two formalisms. It is showed that satisfiability of TL-ALCF concepts can be reduced to satisfiability of ALCF(D) concepts. This allows to use the available ALCF(D) tableau calculus for reasoning with TL-ALCF. Furthermore, it allows to settle the complexity of satisfiability of TL-ALCF concepts, which was previously unknown. +
In this paper, we investigate the relationship between two decidable interval-based temporal description logics that have been proposed in the literature, TL-ALCF and ALCF(A). Although many aspects of these two logics are quite similar, the two logics suggest two rather different paradigms for representing temporal conceptual knowledge. In this paper, we exhibit a reduction from TL-ALCF concepts to ALCF(A) concepts that serves two purposes: first, it nicely illustrates the relationship between the two knowledge representation paradigms; and second, it provides a tight PSpace upper bound for TL-ALCF concept satisfiabiliy, whose complexity was previously unknown. +
In this paper, we summarise our results on Modelling Dynamics in Semantic Web Knowledge Graphs published at WWW 2018 where we proposed a novel data-driven schema for graphs and apply it for the use-case of predicting high-level changes in Wikidata. +
Indexing video data is essential for providing content based access. In this paper, we consider how database technology can offer an integrated framework for modeling and querying video data. As many concerns in video (e.g., modeling and querying) are also found in databases, databases provide an interesting angle to attack many of the problems. From a video applications perspective, database systems provide a nice basis for future video systems. More generally, database research will provide solutions to many video issues even if these are partial or fragmented. From a database perspective, video applications provide beautiful challenges. Next generation database systems will need to provide support for multimedia data (e.g., image, video, audio). These data types require new techniques for their management (i.e., storing, modeling, querying, etc.). Hence new solutions are significant. This paper develops a data model and a rule-based query language for video content based indexing and retrieval. The data model is designed around the object and constraint paradigms. A video sequence is split into a set of fragments. Each fragment can be analyzed to extract the information (i.e., symbolic descriptions) of interest that can be put into a database. This database can then be searched to find information of interest. Two types of information are considered: (1) the entities (i.e., objects) of interest in the domain of a video sequence, (2) video frames which contain these entities. To represent these information, our data model allows facts as well as objects and constraints. We present a declarative, rule-based, constraint query language that can be used to infer relationships about information represented in the model. The language has a clear declarative and operational semantics. +
