Seminars 2016

29.09.2016
Title: A Faster Tableau for CTL*
Speaker: Mark Reynolds , Head of the School of Computer Science and Software Engineering at The University of Western Australia. 
Abstract: There have been several recent suggestions for tableau systems for deciding satisfiability in the practically important branching time temporal logic known as CTL*. In this talk we present a streamlined and more traditional tableau approach built upon the author's earlier theoretical work. Soundness and completeness results are proved. A prototype implementation demonstrates the significantly improved performance of the new approach on a range of test formulas. We also see that it compares favourably to state of the art, game and automata based decision procedures.

28.09.2016
Title: A new rule for LTL tableaux
Speaker: Mark Reynolds, Head of the School of Computer Science and Software Engineering at The University of Western Australia
Abstract: Propositional linear time temporal logic (LTL) is the standard temporal logic for computing applications and many reasoning techniques and tools have been developed for it. Tableaux for deciding satisfiability have existed since the 1980s. However, the tableaux for this logic do not look like traditional tree-shaped tableau systems and their processing is often quite complicated. 
In this talk, we introduce a novel style of tableau rule which supports a new simple traditional-style tree-shaped tableau for LTL. We prove that it is sound and complete. As well as being simple to understand, to introduce to students and to use, it is also simple to implement and is competitive against state of the art systems. It is particularly suitable for parallel implementations.  

15.09.2016
Title: Knowledge Acquisition and Discovery in Description Logics with Formal Concept Analysis
Speaker: Francesco Kriegel,  Technische Universität Dresden, Germany
Abstract:  Description Logics (DLs) are a family of conceptual languages suitable for knowledge representation and reasoning that have a strong logical foundation for which the decidability and complexity of common reasoning problems is widely explored.  In particular, the reasoning tasks allow for a deduction of implicit knowledge from explicitly stated facts and axioms, and plenty of appropriate algorithms were developed and implemented, e.g., tableaux algorithms, and completion algorithms.  DLs provide the logical underpinning of the Web Ontology Language (OWL) and some of its fragments, which are used for the Semantic Web and Linked Data, e.g., in the medical domain (SNOMED ontology), and in DBpedia as well as Wikidata (structured machine-readable derivations of Wikipedia) Furthermore, DLs allow for the expression of assertional and terminological knowledge, and an interesting problem is the (semi-)automatic deduction of terminological facts, so called general concept inclusions (GCIs), from given assertional facts.  This problem may also be varied by taking into account existing terminological facts.  In this talk, we will explore the application of methods from Formal Concept Analysis (FCA) for tackling this problem for three different settings of the input data.  In particular, we show how canonical implicational bases of suitable formal contexts or closure operators yield bases of GCIs for the input data.  More specifically, we utilize suprema and infima of specific closure operators in the lattice of DL concept descriptions, and enumerate their canonical implicational base in order to generate the hidden terminological knowledge in a sound and complete manner.  There is an algorithm that is able to solve this enumeration problem in a highly parallel way where no communication or synchronization between concurrent threads in necessary.

17.05.2016
Title: Recommending Remedial Learning Materials to the Students by Filling their Knowledge Gaps
Speaker: Alexander Tuzhilin, Stern School of Business NYU
Abstract: A new content-based method of providing recommendations of remedial learning materials to the students will be presented. This method identifies gaps in students’ knowledge of the subject matter in the online courses that they take and provides recommendations of relevant targeted educational materials from the library of assembled learning materials to them in order to close the “gaps” in what the students have learned in the course. The proposed recommendation method is empirically validated using a randomized controlled experiment on the students from an online university. It is shown that the students not only liked the recommendations provided to them by the proposed method, but that these recommendations led to better performance results on the final exams for certain segments of the student body.This is joint work with Konstantin Bauman.

31.03.2016
Title: Can we mitigate the attacks on Distance-Bounding Protocols  by using challenge-response rounds repeatedly? 
Speaker: Max Kanovich, professor of computer science at Department of Computer Science and Information Systems, University of London, visiting professor of Faculty of Computer Science,School of Data Analysis and Artificial Intelligence
Abstract: The core of  Distance-Bounding Protocols  is a kind of the challenge-response sub-protocol  to identify the participants, Prover and Verifier. The aim of the talk is twofold:

 1. First, for a typical challenge-response protocol, presented here, we give a full probabilistic analysis of an attack ``between ticks'', newly established by Max Kanovich, Tajana Ban Kirigin,   Vivek Nigam, Andre Scedrov, and Carolyn Talcott.Their attack is based on the discrepancy between the  'observable' challenge-response time interval  and the 'actual' challenge-response time interval;  the dicrepancy is caused by inconsistency  between the continuous time in nature and  the discrete time within the computer clock.

 2. Secondly, we challenge a kind of a general belief that  within Distance-Bounding Protocols  Verifier can improve their performance  by means of collecting statistics in a series  of independent challenge-response rounds  aiming to observe an  ``acceptance challenge-response event''  in the majority of the rounds.

The novelty of our approach is that here we get quite surprising results to support such a claim as well as  to disprove it.

Namely, we show that in the case where  Verifier decides to grant the access by the simple majority, the effect of the  repeated challenge-response rounds  can mitigate the attack but only for  the specific values of the probability  of the erroneous decision in one round.

Whereas in the case where Verifier  decides to grant the access by the large  majority (that is, with gaining a specified  level of support which is greater, say two thirds,  than the threshold of one half used for simple  majority) the idea of repeated challenge-response  rounds works perfectly well for our protocol.  In particular, having observed the ``acceptance challenge-response events''  in the two-thirds majority of rounds,  Verifier can establish the desired upper  bounds for the 'actual' challenge-response  time interval but only with the  high probability

01.02.2016
Title: Reasoning with probability spaces 
Speaker: Stanislav O. Speranski, Scientific Researcher  Laboratory of Logical Systems Sobolev Institute of Mathematics, 
Abstract: Since interest in probabilistic logics has been growing during the last three decades, different sorts of computer scientists and mathematicians — such as Halpern, Keisler, Scott, Terwijn, and others — approach the matter in different ways. In this talk I shall present a formal language L for reasoning about probabilities with quantifiers over events (and over reals if needed), arising very natually from Kolmogorov's notion of probability space. I am going to discuss computational and metamathematical aspects of L. As we shall see, L has many nice features that are not shared by the logics of Halpern and others. Among them are: i) There exists an algorithm for deciding whether a given L-sentence is true in all Lebesgue-like (i.e. atomless) probability spaces or not. ii) Within this framework we can obtain some new results about the relationship between computability and continuity. iii) Further — by analogy with the case of Boolean algebras — we can define `elementary' invariants of probability spaces.

Thus (i) generalises Tarski's famous result that the first-order theory of the ordered field of reals is decidable (which has recently been used to provide computational complexity bounds for certain statistical problems). (ii) leads to a deeper understanding of the above-mentioned relationship (which plays an important role in computing with continuous data and various parts of constructive mathematics). Finally (iii) gives an analogue of the famous elementary classification of Boolean algebras — this throws new light on foundational issues in reverse mathematics (which is an influential research programme in logic and computability).