Towards a Logic-Based Framework for Analyzing Stream Reasoning

Thomas Eiter (Knowledge Based Systems Group, TU Wien)thomas_eiter

The rise of smart applications has drawn interest to logical reasoning over data streams. Recently, different query languages and engines for stream processing respectively stream reasoning were proposed in different communities. However, due to a lack of theoretical foundations, the expressiveness and semantics of diverse approaches was given only informally, and their semantic relationship. Towards clear specifications and means for analytic study, a formal framework is desired that allows to characterize their semantics in precise terms. Inspired by this, we develop a logic-based such framework, which features window operators that provide a flexible mechanism to represent views on streaming data and temporal operators over windows, which also may be nested. In addition, we define a rule language on top. We present the emerging formalism on examples and discuss some complexity issues for it. Furthermore, we briefly consider its usage and relationship to stream query respectively streams reasoning languages, in particular to the Continuous Query Language (CQL) and ETALIS.  We finally address recent results and ongoing research around LARS, which is carried out in a project funded by the Austrian Science Fund.

Querying Ontology Knowledge Bases using Datalog

Thomas Eiter (Knowledge Based Systems Group, TU Wien)thomas_eiter

Description logics play a dominant role in the formalization of ontologies for practical applications of computer science, and they provide, for instance, the formal underpinning of the Web Ontology Language (OWL) recommended by the World Wide Web consortium (W3C). While description logics had been initially targeted at reasoning about conceptual knowledge, in the last decade querying description logic knowledge bases (often simply called ontologies) to elicit information about individuals similar as from databases has received growing attention. Different techniques for query answering have been proposed, among them also to query rewriting to Datalog, which is a well-established query language for relational databases that has several effective reasoning engines available. We consider particular query types, instance and conjunctive queries, which for several description logics have been transformed to Datalog, among them ones underlying the OWL 2 Profiles.  These transformations can also be beneficially exploited for extensions of ontologies, such as in combinations with rules, and have led to research prototype implementations. To exploit and extend the Datalog approach to query answering is an active area, which provides a number of research opportunities.


New directions in typelogical semantics

Michael Moortgat (Universiteit Utrecht)michael_moortgat

Typelogical grammars are substructural logics that provide a prooftheoretic perspective on natural language syntax and semantics. In this tutorial I discuss two recent developments in this area. The first (see [1] and much subsequent work) is the integration of Montague-style compositional interpretation with a vector-based account of lexical meanings. The second development ([2] and subsequent work) systematically extends the vocabulary of Lambek’s original calculus: next to composition (‘merge’) and its residuals, one adds decomposition and subtraction, and a set of unary operators (related to the ‘!’ of linear logic) licensing limited forms of reordering/restructuring that leave the form-meaning correspondence intact. I will discuss the connection between these two developments and the opportunities for transfer of results from one to the other.

[1] B. Coecke, M. Sadrzadeh, and S. Clark. Mathematical foundations for a compositional distributional model of meaning. CoRR, abs/1003.4394,2010.
[2] M. Moortgat. Symmetric categorial grammar. J. Philosophical Logic, 38(6):681–710, 2009.

Cut-elimination in generalisations of the sequent calculus

Revantha Ramanayake (TU Wien)OLYMPUS DIGITAL CAMERA

Logic is concerned with the study and use of valid reasoning. The most well-known logics are classical propositional and first-order logic. Nevertheless, various other forms of reasoning are needed to model the different applications and situations that arise in practice, giving rise to many new logics (‘non-classical logics’) that are more expressive and permit finer distinctions than classical logic. The study of such logics is interesting in its own right and also yields an understanding of the systems modelled by these logics.

The basis of the proof-theoretical approach to studying a logic is the notion of proof, and in particular, the study of the formal proof systems of the logic (a statement belongs to the logic if and only if it has a proof in such a proof system). Gentzen introduced the formal proof-system called the sequent calculus in order to study the structure of proofs in classical and intuitionistic logic. His celebrated cut-elimination theorem implies the sub-formula property which states that a statement can be proved in the calculus using only sub-formulae of the formulae occurring in the statement. The point is that the proofs from his calculus have a nice normal form (such calculi are called analytic). Contrast, for example, with proofs in the Hilbert calculus where formulae that occur in the proof might not occur in the statement that is proved. Gentzen made use of his result to give a formal proof of consistency of Peano arithmetic using a suitable induction principle.

Note that if we are not interested in having a calculus with the subformula property, then it is easy to obtain a sequent calculus for most logics of interest. However the key to a proof-theoretical study of the logic is an analytic calculus. For many logics of interest it is not clear at all how to obtain an analytic sequent calculus. This has led to the introduction of various generalisations and extensions of the sequent calculus. These generalisations yield analytic calculi for some logics and not for others and it is still not clear why cut-elimination seems to fail for certain logics in certain formal systems (negative results stating that a given formal system cannot yield an analytic calculus for a certain logic are rare!).

In this tutorial I will discuss two generalisations of the sequent calculus: the hypersequent calculus and the Display Calculus. I will pay special attention to the display calculus which has been used to provide analytic formal systems for many different non-classical logics. An attractive feature of the display calculus is the natural general cut-elimination theorem which applies whenever the rules of the calculus satisfy certain easy to check conditions. I will ‘take apart’ the display calculus in order to motivate why the rules of calculus take the shape that they do, and why this leads to a general cut-elimination theorem. I will then explain how a display calculus for a logic can be extended by suitable new rules to obtain a display calculi for axiomatic extensions of that logic. The preservation of analyticity under the addition of new rules is known as modularity and this property usually fails in the sequent calculus but holds for the rules of the display calculus we introduce here. An intention of this tutorial is that the insights on proof systems and cut-elimination explained via the display calculus will be applicable to various other proof systems as well.

Complexity in Logic: off the beaten track towards pastures new

Uli Sattler (University of Manchester)OLYMPUS DIGITAL CAMERA

Research in logic is hard: first, there are loads of existing formalisms, their relationships, model properties, computational complexity classes, etc. that we have to learn about and understand. Then, there is a wide range of skills to acquire, including writing, note keeping, proof techniques, and analytical thinking. Of course, we need to narrow down an interesting yet solvable research question and make progress towards its solution. Many of these questions are basically “what is the computational complexity of problem X in logic Y?”. In my tutorial, I will first describe the above sources of complexity in more detail, and then present some interesting cases where starting from but straying from this “beaten track” of computational complexity has resulted in interesting insights. These cases include new reasoning problems or tasks, and also alternative measures of complexity.

Answer Set Solving in a nutshell

Torsten Schaub (University Potsdam)OLYMPUS DIGITAL CAMERA

The tutorial aims at acquainting the participant with ASP’s modeling and solving methodology, enabling her/him to conduct independent problem solving using ASP systems. To this end, the tutorial starts with a brief introduction to the essential formal concepts of ASP, needed for understanding its semantics and solving technology. In fact, ASP solving rests on two major components: A grounder turning specifications in ASP’s modeling language into propositional logic programs and a solver computing a requested number of answer sets of the program. We illustrate both ASP’s grounding techniques and the basic ideas of the underlying solving technology. Finally, we sketch the usage of ASP in conjunction with Python for modeling complex reasoning scenarios. This involves an introduction to the API of clingo 4, an ASP system with control capacities expressible in Python. We illustrate this by developing the board game of Ricochet Robots.

All involved ASP systems are freely available from http://potassco.sourceforge.net.