This workshop takes place on the occasion of Raoul Koudijs' PhD defense. It features talks about deriving and/or revising logical concept based on data examples, as well as an introductory talk about Dafny, a Hoare-logic inspired language used for the formal specification and verification of programs.

Workshop location: Spinoza room, UBA (University Library), Vendelstraat 2-8 Amsterdam

Workshop Schedule:

9:15-9:30 Welcome and coffee

9:30-10:00 Jean Christoph Jung: “Separation Problems for Temporal Instance Queries”

10:00-10:30 Ana Ozaki: "Model Change for Description Logic Concepts"

10:30-11:00 Montserrat Hermo (over zoom): "An introduction to Dafny"

11:00-12:00 General discussion 

13:00 Raoul's PhD Defense (location: Agnietenkapel)

Jean Christoph Jung (TU Dortmondt):

Separation Problems for Temporal Instance Queries

The separation problem for a class Q of database queries is to find a query in Q that distinguishes between a given set of `positive' and `negative' data examples. A separating query provides explanations of examples and underpins the query-by-example paradigm to support database users in constructing and refining queries. As the space of all separating queries can be large, it is helpful to succinctly represent this space by means of its most specific (logically strongest) and general (weakest) members. We investigate this extremal separation problem for classes of instance queries formulated in linear temporal logic LTL with the operators conjunction, next, and eventually. Our results range from tight complexity bounds for verifying and counting extremal separators to algorithms computing them.

Joint work with Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev.

Ana Ozaki (University of Oslo):

Model Change for Description Logic Concepts

We consider the problem of modifying a description logic concept in light of models represented as pointed interpretations. We call this setting model change, and distinguish three main kinds of changes: eviction, which consists of only removing models; reception, which incorporates models; and revision, which combines removal with incorporation of models in a single operation. We introduce a formal notion of revision and argue that it does not reduce to a simple combination of eviction and reception, contrary to intuition. We provide positive and negative results on the compatibility of eviction and reception for EL and ALC description logic concepts and on the compatibility of revision for ALC concepts.

Joint work with Jandson Ribeiro. 

Montserrat Hermo (University of the Basque Country):

An introduction to Dafny

I will introduce Dafny, a programming language that provides integrated support for formal specification and verification. Dafny lets you write annotations in the style of Hoare logic—such as pre- and postconditions, loop invariants, and termination checks. Proofs can be verified instantaneously, by compiling to the Boogie intermediate language, which uses the Z3 SMT-solver to discharge proof obligations. The presentation will be based on examples, including the soundness and completeness  (proved in Dafny) of a proof system that decides the model-checking problem for the fragment of first-order logic FO(∀, ∃, ∧).