Boris Konev

IJCAI Conference 2023 Conference Paper

Reverse Engineering of Temporal Queries Mediated by LTL Ontologies

• Marie Fortin
• Boris Konev
• Vladislav Ryzhikov
• Yury Savateev
• Frank Wolter
• Michael Zakharyaschev

In reverse engineering of database queries, we aim to construct a query from a given set of answers and non-answers; it can then be used to explore the data further or as an explanation of the answers and non-answers. We investigate this query-by-example problem for queries formulated in positive fragments of linear temporal logic LTL over timestamped data, focusing on the design of suitable query languages and the combined and data complexity of deciding whether there exists a query in the given language that separates the given answers from non-answers. We consider both plain LTL queries and those mediated by LTL ontologies.

KR Conference 2022 Conference Paper

Interpolants and Explicit Definitions in Extensions of the Description Logic EL

• Marie Fortin
• Boris Konev
• Frank Wolter

We show that the vast majority of extensions of the description logic EL do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for EL with nominals, EL with the universal role, EL with role hierarchies and transitive roles, and for ELI. It follows in particular that the existence of an explicit definition of a concept or individual name cannot be reduced to subsumption checking via implicit definability. We show that nevertheless the existence of interpolants and explicit definitions can be decided in polynomial time for standard tractable extensions of EL (such as EL++) and in ExpTime for ELI and various extensions. It follows that these existence problems are not harder than subsumption which is in sharp contrast to the situation for expressive DLs. We also obtain tight bounds for the size of interpolants and explicit definitions and the complexity of computing them: single exponential for tractable standard extensions of EL and double exponential for ELI and extensions. We close with a discussion of Horn-DLs such as Horn-ALCI.

KR Conference 2022 Conference Paper

Unique Characterisability and Learnability of Temporal Instance Queries

• Marie Fortin
• Boris Konev
• Vladislav Ryzhikov
• Yury Savateev
• Frank Wolter
• Michael Zakharyaschev

We aim to determine which temporal instance queries can be uniquely characterised by a (polynomial-size) set of positive and negative temporal data examples. We start by considering queries formulated in fragments of propositional linear temporal logic LTL that correspond to conjunctive queries (CQs) or extensions thereof induced by the until operator. Not all of these queries admit polynomial characterisations, but by imposing a further restriction to path-shaped queries we identify natural classes that do. We then investigate how far the obtained characterisations can be lifted to temporal knowledge graphs queried by 2D languages combining LTL with concepts in description logics EL or ELI (i. e. , tree-shaped CQs). While temporal operators in the scope of description logic constructors can destroy polynomial characterisability, we obtain general transfer results for the case when description logic constructors are within the scope of temporal operators. Finally, we apply our characterisations to establish (polynomial) learnability of temporal instance queries using membership queries in the active learning framework.

JMLR Journal 2018 Journal Article

Exact Learning of Lightweight Description Logic Ontologies

• Boris Konev
• Carsten Lutz
• Ana Ozaki
• Frank Wolter

We study the problem of learning description logic (DL) ontologies in Angluin et al.'s framework of exact learning via queries. We admit membership queries (“is a given subsumption entailed by the target ontology?”) and equivalence queries (“is a given ontology equivalent to the target ontology?”). We present three main results: (1) ontologies formulated in (two relevant versions of) the description logic DL-Lite can be learned with polynomially many queries of polynomial size; (2) this is not the case for ontologies formulated in the description logic $\mathcal{E}\mathcal{L}$, even when only acyclic ontologies are admitted; and (3) ontologies formulated in a fragment of $\mathcal{E}\mathcal{L}$ related to the web ontology language OWL 2 RL can be learned in polynomial time. We also show that neither membership nor equivalence queries alone are sufficient in cases (1) and (3). [abs] [ pdf ][ bib ] &copy JMLR 2018. ( edit, beta )

KR Conference 2018 Conference Paper

ExactLearner: a Tool for Exact Learning of EL Ontologies

• Ricardo Duarte
• Boris Konev
• Ana Ozaki

We present ExactLearner, a tool for exactly learning and teaching EL terminologies. The learning protocol follows Angluin’s exact learning model, where an ontology engineer tries to identify an ontology by interacting with a domain expert by asking queries. We implement the learning process as a question-answer game between two components of our system, the learner and the teacher. We evaluate ExactLearner’s performance on EL ontologies from the Oxford ontology repository and demonstrate that despite the algorithm being exponential, it successfully terminates for small and medium size ontologies. We investigate the impact of various learner and teacher features and identify those most useful for learning.

AAAI Conference 2016 Conference Paper

A Model for Learning Description Logic Ontologies Based on Exact Learning

• Boris Konev
• Ana Ozaki
• Frank Wolter

We investigate the problem of learning description logic (DL) ontologies in Angluin et al. ’s framework of exact learning via queries posed to an oracle. We consider membership queries of the form “is a tuple a of individuals a certain answer to a data retrieval query q in a given ABox and the unknown target ontology? ” and completeness queries of the form “does a hypothesis ontology entail the unknown target ontology? ”. Given a DL L and a data retrieval query language Q, we study polynomial learnability of ontologies in L using data retrieval queries in Q and provide an almost complete classification for DLs that are fragments of EL with role inclusions and of DL-Lite and for data retrieval queries that range from atomic queries and EL/ELI-instance queries to conjunctive queries. Some results are proved by non-trivial reductions to learning from subsumption examples.

KR Conference 2016 Conference Paper

Anti-Unification of Concepts in Description Logic EL

• Boris Konev
• Temur Kutsia

We study anti-unification for the description logic EL and introduce the notion of least general generalisation, which generalises simultaneously least common subsumer and concept matching. The idea of generalisation of two concepts is to detect maximal similarities between them, and to abstract over their differences uniformly. We demonstrate that a finite minimal complete set of generalisations for EL concepts always exists and establish complexity bounds for computing them. We present an anti-unification algorithm that computes generalisations with a fixed skeleton, study its properties and report on preliminary experimental evaluation.

IJCAI Conference 2016 Conference Paper

Conservative Rewritability of Description Logic TBoxes

• Boris Konev
• Carsten Lutz
• Frank Wolter
• Michael Zakharyaschev

We investigate the problem of conservative rewritability of a TBox T in a description logic L into a TBox T' in a weaker description logic L'. We focus on model-conservative rewritability (T' entails T and all models of T are expandable to models of T'), subsumption-conservative rewritability (T' entails T and all subsumptions in the signature of T entailed by T' are entailed by T), and standard description logics between ALC and ALCQI. We give model-theoretic characterizations of conservative rewritability via bisimulations, inverse p-morphisms and generated subinterpretations, and use them to obtain a few rewriting algorithms and complexity results for deciding rewritability.

AIJ Journal 2015 Journal Article

Computer-aided proof of Erdős discrepancy properties

• Boris Konev
• Alexei Lisitsa

IROS Conference 2015 Conference Paper

Scalable distributed collaborative tracking and mapping with Micro Aerial Vehicles

• Richard Williams
• Boris Konev
• Frans Coenen

This paper describes work on a distributed framework for collaborative multi-robot localisation and mapping with large teams of Micro Aerial Vehicles (MAVs). We demonstrate the benefits of running both image capture and frame-to-frame tracking on the same device while offloading the more computationally intensive aspects of map creation and optimization to an off-board computer. We show no impact on the accuracy of pose estimates of this distributed approach and indeed demonstrate a robustness to delay that improves localisation performance. The bandwidth requirements of our system are much lower than similar systems which enables us to accommodate larger teams of MAVs. In the results section we demonstrate the performance of our system in both simulated and real-world environments.

SAT Conference 2014 Conference Paper

A SAT Attack on the Erdős Discrepancy Conjecture

• Boris Konev
• Alexei Lisitsa 0001

Abstract In 1930s Paul Erdős conjectured that for any positive integer C in any infinite ±1 sequence ( x n ) there exists a subsequence x d, x 2 d, x 3 d, …, x kd, for some positive integers k and d, such that \(\mid \sum_{i=1}^k x_{id} \mid >C\). The conjecture has been referred to as one of the major open problems in combinatorial number theory and discrepancy theory. For the particular case of C = 1 a human proof of the conjecture exists; for C = 2 a bespoke computer program had generated sequences of length 1124 of discrepancy 2, but the status of the conjecture remained open even for such a small bound. We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solver, one can obtain a discrepancy 2 sequence of length 1160 and a proof of the Erdős discrepancy conjecture for C = 2, claiming that no discrepancy 2 sequence of length 1161, or more, exists. We also present our partial results for the case of C = 3.

KR Conference 2014 Conference Paper

Exact Learning of Lightweight Description Logic Ontologies

• Boris Konev
• Carsten Lutz
• Ana Ozaki
• Frank Wolter

data with the aim of including them in the ontology. Some We study learning of description logic TBoxes in Angluin et al. ’s framework of exact learning via queries. We admit entailment queries (“is a given subsumption entailed by the target TBox? ”) and equivalence queries (“is a given TBox equivalent to the target TBox? ”), assuming that the signature and logic of the target TBox are known. We present three main results: (1) TBoxes formulated in DL-Lite with role inclusions and composite concepts on the right-hand side of concept inclusions can be learned in polynomial time; (2) EL TBoxes with only concept names on the right-hand side of concept inclusions can be learned in polynomial time; and (3) EL TBoxes cannot be learned in polynomial time. It follows that non-polynomial time learnability of EL TBoxes is caused by the interaction between existential restrictions on the rightand left-hand sides of concept inclusions. We also show that neither entailment nor equivalence queries alone are sufficient in cases (1) and (2) above.

ECAI Conference 2014 Conference Paper

Lower and Upper Approximations for Depleting Modules of Description Logic Ontologies

• William Gatens
• Boris Konev
• Frank Wolter

It is known that no algorithm can extract the minimal depleting Σ -module from ontologies in expressive description logics (DLs). Thus research has focused on algorithms that approximate minimal depleting modules 'from above' by computing a depleting module that is not necessarily minimal. The first contribution of this paper is an implementation (AMEX) of such a depleting module extraction algorithm for expressive acyclic DL ontologies that uses a QBF solver for checking conservative extensions relativised to singleton interpretations. To evaluate AMEX and other module extraction algorithms we propose an algorithm approximating minimal depleting modules 'from below' (which also uses a QBF solver). We present experiments based on NCI (the National Cancer Institute Thesaurus) that indicate that our lower approximation often coincides with (or is very close to) the upper approximation computed by AMEX, thus proving for the first time that an approximation algorithm for minimal depleting modules can be almost optimal on a large ontology. We use the same technique to evaluate locality-based module extraction and a hybrid approach on NCI.

KR Conference 2014 Conference Paper

Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference

• Michel Ludwig
• Boris Konev

the ontology structure. Ontology obfuscation: in software engineering, obfuscation (Collberg, Thomborson, and Low 1998) transforms a given program into a functionally equivalent one that is more difficult to read and understand for humans for the purpose of preventing reverse engineering. Forgetting can provide a similar function in the context of ontology engineering. Terms are often defined with the help of auxiliary terms which give structure to TBox inclusions. However, such a structure might be considered proprietary knowledge that should not be exposed, or it could simply be of little interest for ontology users. By forgetting these intermediate auxiliary terms, we obtain an ontology that is functionally equivalent, yet harder to read, understand, and modify by humans. Further applications of forgetting can be found in (Konev, Walther, and Wolter 2009; Lutz, Seylan, and Wolter 2012). We develop a clausal resolution-based approach for computing uniform interpolants of TBoxes formulated in the description logic ALC when such uniform interpolants exist. We also present an experimental evaluation of our approach and of its application to the logical difference problem for real-life ALC ontologies. Our results indicate that in many practical cases uniform interpolants exist and that they can be computed with the presented algorithm.

AIJ Journal 2013 Journal Article

Model-theoretic inseparability and modularity of description logic ontologies

• Boris Konev
• Carsten Lutz
• Dirk Walther
• Frank Wolter

TIME Conference 2012 Conference Paper

Symmetric Temporal Theorem Proving

• Amir Niknafs-Kermani
• Boris Konev
• Michael Fisher 0001

In this paper we consider the deductive verification of propositional temporal logic specifications of symmetric systems. In particular, we provide a heuristic approach to the scalability problems associated with analysing properties of large numbers of processes. Essentially, we use a temporal resolution procedure to verify properties of a system with few processes and then generalise the outcome in order to reduce the verification complexity of the same system with much larger numbers of processes. This provides a practical route to deductive verification for many systems comprising identical processes.

AAAI Conference 2011 Conference Paper

Conjunctive Query Inseparability of OWL 2 QL TBoxes

• Boris Konev
• Roman Kontchakov
• Michel Ludwig
• Thomas Schneider
• Frank Wolter
• Michael Zakharyaschev

The OWL 2 profile OWL 2 QL, based on the DL-Lite family of description logics, is emerging as a major language for developing new ontologies and approximating the existing ones. Its main application is ontology-based data access, where ontologies are used to provide background knowledge for answering queries over data. We investigate the corresponding notion of query inseparability (or equivalence) for OWL 2 QL ontologies and show that deciding query inseparability is PSPACE-hard and in EXPTIME. We give polynomial time (incomplete) algorithms and demonstrate by experiments that they can be used for practical module extraction.

KR Conference 2010 Conference Paper

Decomposing Description Logic Ontologies

• Boris Konev
• Carsten Lutz
• Denis Ponomaryov
• Frank Wolter

Recent years have seen the advent of large and complex ontologies, most notably in the medical domain. As a consequence, structuring mechanisms for ontologies are nowadays viewed as an indispensible tool. A basic such mechanism is the automatic decomposition of the vocabulary of an ontology into independent parts. In this paper, we study decompositions that are syntax independent in the sense that the resulting partitioning depends only on the meaning of the vocabulary items, but not on the concrete syntactic form of the axioms in the ontology. We present the first systematic investigation of decompositions of this type in the context of ontologies. Specifically, we focus on ontologies formulated in description logics and provide a variety of results that range from theorems stating the existence of unique finest decompositions to complexity results and algorithms computing decompositions. We also investigate the relationship between the existence of unique finite decompositions and a variant of the Craig interpolation property called parallel interpolation.

IJCAI Conference 2009 Conference Paper

• Boris Konev
• Dirk Walther
• Frank Wolter

We develop a framework for forgetting concepts and roles (aka uniform interpolation) in terminologies in the lightweight description logic EL extended with role inclusions and domain and range restrictions. Three different notions of forgetting, preserving, respectively, concept inclusions, concept instances, and answers to conjunctive queries, with corresponding languages for uniform interpolants are investigated. Experiments based on SNOMED CT (Systematised Nomenclature of Medicine Clinical Terms) and NCI (National Cancer Institute Ontology) demonstrate that forgetting is often feasible in practice for largescale terminologies.

TIME Conference 2008 Conference Paper

Practical First-Order Temporal Reasoning

• Clare Dixon
• Michael Fisher 0001
• Boris Konev
• Alexei Lisitsa 0001

In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for this form of specification and tractable enough for practical deductive verification. Importantly, the power of the temporal language allows us to describe (and verify) asynchronous systems, communication delays and more complex liveness and fairness properties. These aspects appear difficult for many other approaches to infinite-state verification.

ECAI Conference 2008 Conference Paper

Semantic Modularity and Module Extraction in Description Logics

• Boris Konev
• Carsten Lutz
• Dirk Walther 0002
• Frank Wolter

The aim of this paper is to study semantic notions of modularity in description logic (DL) terminologies and reasoning problems that are relevant for modularity. We define two notions of a module whose independence is formalised in a model-theoretic way. Focusing mainly on the DLs ℰ ℒ and 𝒜 ℒ 𝒞 , we then develop algorithms for module extraction, for checking whether a part of a terminology is a module, and for a number of related problems. We also analyse the complexity of these problems, which ranges from tractable to undecidable. Finally, we provide an experimental evaluation of our module extraction algorithms based on the large-scale terminology SNOMED CT.

IJCAI Conference 2007 Conference Paper

• Clare Dixon
• Michael Fisher
• Boris Konev

Temporal reasoning is widely used within both Computer Science and A. I. However, the underlying complexity of temporal proof in discrete temporal logics has led to the use of simplified formalisms and techniques, such as temporal interval algebras or model checking. In this paper we show that tractable sub-classes of propositional linear temporal logic can be developed, based on the use of XOR fragments of the logic. We not only show that such fragments can be decided, tractably, via clausal temporal resolution, but also show the benefits of combining multiple XOR fragments. For such combinations we establish completeness and complexity (of the resolution method), and also describe how such a temporal language might be used in application areas, for example the verification of multi-agent systems. This new approach to temporal reasoning provides a framework in which tractable temporal logics can be engineered by intelligently combining appropriate XOR fragments.

TIME Conference 2006 Conference Paper

Is There a Future for Deductive Temporal Verification?

• Clare Dixon
• Michael Fisher 0001
• Boris Konev

In this paper, we consider a tractable sub-class of propositional linear time temporal logic, and provide a complete clausal resolution calculus for it. The fragment is important as it can be used to represent simple Buchi automata. We also show that, just as the emptiness check for a Buchi automaton is tractable, the complexity of deciding unsatisfiability, via resolution, of our logic is polynomial (rather than exponential). Consequently, a Buchi automaton can be represented within our logic, and its emptiness can be tractably decided via deductive methods. This may have a significant impact upon approaches to verification, since techniques such as model checking inherently depend on the ability to check emptiness of an appropriate Buchi automaton. Thus, we also discuss how such a logic might form the basis for practical deductive temporal verification

JELIA Conference 2006 Conference Paper

On Herbrand's Theorem for Intuitionistic Logic

• Alexander V. Lyaletski
• Boris Konev

Abstract In this paper we reduce the question of validity of a first-order intuitionistic formula without equality to generating ground instances of this formula and then checking whether the instances are deducible in a propositional intuitionistic tableaux calculus, provided that the propositional proof is compatible with the way how the instances were generated. This result can be seen as a form of the Herbrand theorem, and so it provides grounds for further theoretical investigation of computer-oriented intuitionistic calculi.

LPAR Conference 2003 Conference Paper

Handling Equality in Monodic Temporal Resolution

• Boris Konev
• Anatoli Degtyarev
• Michael Fisher 0001

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments including the guarded fragment with equality. In this paper, we specialise the monodic resolution method to the guarded monodic fragment with equality and first-order temporal logic over expanding domains. We introduce novel resolution calculi that can be applied to formulae in the normal form associated with the clausal resolution method, and state correctness and completeness results.

TIME Conference 2003 Conference Paper

Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case

• Boris Konev
• Anatoli Degtyarev
• Clare Dixon
• Michael Fisher 0001
• Ullrich Hustadt

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.