Applications of Logics in Artificial Intelligence ALAI 2013
Department of Mathematics and Computer Science
University of Catania, Italy
Talk:
The Satisfiability Problem for Quantified Stratified Syllogistics with Applications to Modal LogicAbstract:
We introduce two multi-sorted stratified syllogistics (called 3LQS R and 4LQS R, respectively) admitting variables of three and four sorts, respectively, and a restricted form of quantification over variables of sorts 0, 1, 2 (and 3, respectively), and prove that they enjoy a small model property, thereby establishing the solvability of their satisfiability problems.
We also show that the collections of suitably constrained formulae of 3LQS R and 4LQS R, satisfying certain syntactical constraints and whose quantifier prefixes have length bounded by a constant, have an NP-complete satisfiability problem. Finally we show that the modal logics S5 and K45 can be expressed in such restricted fragments.
Barbara Dunin-Kęplicz and Alina Strachocka
Institute of Informatics
University of Warsaw, Poland
Talk:
Perceiving Rules Under Incomplete and Inconsistent InformationAbstract:
This presentation extends an implementation of the speech act assert in a paraconsistent framework by providing means for agents to perceive and learn not only facts, but also rules. A natural four-valued model of interaction yields multiple new cognitive situations. They are analyzed in the context of communicative relations, which play a role in determining the admissibility of a rule. The particular choice of a rule-based, DATALOG::-like query language 4QL as a four-valued implementation framework ensures that, in contrast to the standard two-valued approaches, tractability of the model is maintained.
Ivo Düntsch
Computer Science Department
Brock University, Canada
Talk:
Qualitative Spatial ReasoningAbstract:
Based on ideas put forward in the early 20th century, qualitative spatial reasoning (QSR) as a field of artificial intelligence has evolved in the 1990s, and it is concerned with the qualitative aspects of representing – and reasoning about – spatial and temporal entities such as regions or time interval as opposed to emphasis on one-dimensional situations such as point. Applications of QSR can be found in geographical information systems, spatial query languages, natural languages, robotics, and many other fields. I will give an introductory overview of the history and current state of QSR.
Anna Gomolińska
Computer Science Institute
University of Bialystok, Poland
Talk:
Rough Inclusion Functions and Their Role in Granular ComputingAbstract:
Rough inclusion, first introduced axiomatically by L. Polkowski and A. Skowron in 1994, is a fundamental concept underlying a formal theory called rough mereology. The standard understanding of rough inclusion functions (RIFs) is that they are mappings with which one can measure the degree of inclusion between sets of objects of some universe and which conform to the axioms of rough inclusion.
In this talk, by rough inclusion functions we mean a broader class of functions to measure the degree of inclusion between sets of objects. Such functions play an important role in granular computing, an approach to computation based on the notion of an information granule introduced by L. A. Zadeh. Not only RIFs can be used to measure the degree of inclusion between information granules, but they can also be applied to measure the degree of similarity or nearness between granules, to approximate sets of objects by means of elementary granules or to define graded semantics of formulas specifying properties of information granules. Other applications include, e.g. construction of information granules satisfying a given specification or interaction between information granules. During the talk, several various rough inclusion functions will be presented in detail. Apart from discussion of their properties, we will comment on their origin and possible applications in granular computing.
Beata Konikowska
Institute of Computer Science
Polish Academy of Sciences, Poland
Talk:
From Non-deterministic Semantics to Ordinary Gentzen Sequent CalculiAbstract:
A major generalization of ordinary logical matrices are non-deterministic matrices (Nmatrices) – multiple-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set of options. Thanks to the use of Nmatrices, we can provide finite-valued semantics for many important logics which cannot be characterized by finite ordinary matrices. They include, among others: all logics obtained from the classical logic by deleting some rule(s) from its standard sequent calculus, and all paraconsistent LFIs (Logics of Formal Inconsistency), except those including any of the axioms (l), (d), (o). The crucial advantage is that logics with a finite characteristic Nmatrix enjoy the main good properties possessed by logics with an ordinary (deterministic) finite characteristic matrix.
A converse task is to provide proof systems for logics with semantics based on finite Nmatrices. We describe a general method (based on a weakened version of Rasiowa-Sikorski (R-S) decomposition methodology) for developing sound and complete, cut-free n-sequent systems for all propositional logics with semantics based on finite Nmatrices. If the logic in question satisfies a certain minimal expressiveness condition, we show that above n-sequent calculus can be further translated into an equivalent sound and complete calculus of ordinary sequents. The expressiveness condition is that we must be able to identify the truth-value of any formula φ by determining whether certain formulas uniformly constructed from φ are satisfied (i.e.: have designated values) or not. As any language which does not meet this condition can be extended to one which does, so the procedure is quite general.
References:
1. A. Avron, B. Konikowska, Multi-valued Calculi for Logics Based on Non-determinism, Journal of the Interest Group in Pure and Applied Logic, Vol 10, pp. 365–387, 2005.
2. A. Avron, J. Ben-Naim, B. Konikowska, Cut-free Ordinary Sequent Calculi for Logics Having Generalized Finite-Valued Semantics, Logica Universalis, Vol. 1, Issue 1, pp. 41–70, 2007.
Emilio Munoz-Velasco
Department of Applied Mathematics
University of Malaga, Spain
Talk:
Reasoning with moving objects using a logic approach based on fuzzy qualitative representationAbstract:
A logic approach to reason with moving objects under fuzzy qualitative representation is presented. This approach is able to deal both with qualitative and quantitative information, and consequently, can obtain more accurate results than purely qualitative approaches. The proposed logic system is introduced as an extension of Propositional Dynamic Logic. This fact simplifies the theoretical study concerning soundness, completeness and decidability; and, on the other hand, provides the possibility of constructing complex relations from simpler ones and the use of a language very close to programming languages. Some of the advantages of this approach are explained on the basis of some examples from the literature.
Sinh Hoa Nguyen and Hung Son Nguyen
Institute of Mathematics
University of Warsaw, Poland
Talk:
Support Vector Machines Using Boolean KernelsAbstract:
Rough Sets (RS) and Support Vector Machine (SVM) are the two big and independent research areas in AI. Originally, rough set theory is dealing with the concept approximation problem under uncertainty. The basic idea of RS is related to lower and upper approximations, and it can be applied in classification problem. At the first sight RS and SVM offer different approaches to classification problem. Most RS methods are based on minimal decision rules, while SVM converts the linear classifiers into instance based classifiers. We will present a comparison analysis between these areas and shows that, despite differences, there are quite many analogies in the two approaches. We will show that some rough set classifiers are in fact the SVM with Boolean kernel and propose some hybrid methods that combine the advantages of those two great machine learning methods.
Linh Anh Nguyen
Institute of Informatics
University of Warsaw, Poland
Talk:
ExpTime Tableaux for Graded Converse-PDL Extended with Regular Inclusion AxiomsAbstract:
We present the first ExpTime tableau decision procedure for the modal logic GCPDLreg, which extends propositional dynamic logic with converse, graded modal operators and regular inclusion axioms specified by finite automata. Our decision procedure does not use cuts. It is based on Nguyen's tableau methods for the modal logic CPDLreg and the description logic SHIQ.
Marianna Nicolosi Asmundo
Department of Mathematics and Computer Science
University of Catania, Italy
Talk:
Dual Tableau Decision Procedures for Some Fragments of Relational LogicAbstract:
We analyze two fragments of the relational logic RL(1) characterized by some constraints on the terms having the composition as the leading operator. Specifically, the first argument of the composition is allowed to be either a relational variable or the universal constant 1 in the first fragment, a positive Boolean term allowing the inverse operator and the universal constant 1 in the second one. These logics can be used as formalisms to represent several theories, in particular some non-classical logics including modal and description logics. We introduce a decision procedure based on dual tableaux for both of them. We also present ongoing work concerning dual tableau-based decision procedures for logics of binary relations whose terms allow the complement operation in the first argument of the composition.
Maciej Przybylski
Institute of Automatic Control and Robotics
Warsaw University of Technology, Poland
Talk:
High-level Robot ControlAbstract:
In typical approaches, the high-level control relies on the assumption of an autonomy and determinism of lower level controllers implementing high-level actions, which is insufficient in most of robotic applications. Therefore, a broader view on a robot control system design is necessary. This presentation covers the problem of the high- and low-level robot control. A range of topics, starting from existing systems review, through the role of qualitative reasoning, to some practical aspects of the high-level control in real world robotic applications, will be discussed. A special attention to an integration of high-level (typically qualitative) and low-level (typically quantitative) robot control will be paid. Finally, early stage ideas on the use of high-level reasoning in action planning for the Courier service robot will be presented.
Agustín Valverde and Alfredo Burrieza
Department of Applied Mathematics
University of Malaga, Spain
Talk:
Qualitative Space: Closeness, Medium, FarAbstract:
We introduce a multi-modal logic to work with qualitative concepts of distances without and underlying quantitative notion. In this first approach, we consider three types of distances: "closed", "medium" and "far". Understanding these types of distances as relations between objects (in a plane or in space), we will require properties which are consistent with the notion of closeness we want to express. For example, we consider that the relation associated with "closed" is an equivalence relation. If we apply these concepts to distances within a city, we understand that the nearby locations are those that are in the same neighborhood or district, any couple of places within the same neighborhood is considered close, either at a distance of ten meters or two hundred meters; that is, the equivalence classes would be the different neighborhoods of the city. Following with the same example, we consider that two adjacent neighborhoods are in the middle distance and of course it loses the property of transitivity, since depending on the situation of neighborhoods, going from one to another and to another, we can go very far. Thus, we will consider three modal connectives, c, m and f; the former is defined by an equivalence relation and the other by relations which only require to be symmetrical and additional properties will be considered to capture the possible interactions between them.
Przemysław Wałęga
Institute of Philosophy, University of Warsaw, Poland
Warsaw University of Technology, Poland
Talk:
Combined Probabilistic and Qualitative Reasoning MethodAbstract:
We present the approach that combines probabilistic description of beliefs with their qualitative representation. The system is based on the second-order Situation Calculus formal language that is able to model dynamic changes of situations. We have developed the reasoning method that describes how qualitative beliefs change while actions are performed. The approach is tested in a specific scenario in which the robot's aim is to plan the actions' sequence that leads to a goal achievement. In most cases the given goal is achieved. However, since we consider the incomplete qualitative information, reasoning mistakes occasionally occur. Our method is implemented and may be used in real robotic systems.