ABSTRACT. This extended abstract briefly summarizes our recent work on extending the study of counting queries to Horn description logics outside the DL-Lite family. Through a combination of novel techniques, adaptations of existing constructions, and new connections to closed predicates, we achieve a complete picture of the data and combined complexity of answering counting conjunctive queries (CCQs) and cardinality queries (a restricted class of CCQs) in ELHI⊥ and its various sublogics.

ABSTRACT. In ontology-mediated query answering, access to incomplete data sources is mediated by a conceptual layer constituted by an ontology. To correctly compute answers to queries, it is necessary to perform complex reasoning over the constraints expressed by the ontology. In the literature there exists a multitude of techniques incorporating the ontological knowledge into queries. However, few of these approaches were designed for comprehensibility of the query answers. In this article, we try to bridge these two qualities by adapting a proof framework originally applied to axiom entailment for conjunctive query answering. We investigate the data and combined complexity of determining the existence of a proof below a given quality threshold, which can be measured in different ways. By distinguishing various parameters such as the shape of a query, we obtain an overview of the complexity of this problem for the lightweight ontology languages DL-Lite_{R} and EL.

ABSTRACT. In reverse engineering of database queries, one aims to construct a query from a set of positively and negatively labelled answers and non-answers. The query can then be used to explore the data further or as an explanation of the answers and non-answers. We consider this reverse engineering problem for queries formulated in various fragments of positive linear temporal logic LTL over data instances given by timestamped atomic concepts. We focus on the design of suitable query languages and the complexity of the separability problem: ‘does there exist a query in the given query language that separates the given answers from the non-answers?’. We deal with both plain LTL queries and those that are mediated by ontologies providing background knowledge and formulated in fragments of clausal LTL.

ABSTRACT. Formal verification and model checking in particular is a key technology which is widely used for enabling the fast-growing electronic industry, serving many aspects of our digital lives in communication and computing. The pandemic has helped accelerate the growth of this industry boosted by the global digital orientation and remote collaboration. Analysists estimate that the electronic industry total annual revenue will be doubled by 2030 to reach one Trillion USD. Chip design is the heart of it and spans many areas including handheld devices, computer servers and cloud computing, mobile phones, Artificial Intelligence, Internet-of-things, automotive and variety of embedded systems. Cost of chip design is severely growing on the other hand and the industry consistently looks for solutions to address the productivity gaps. Formal Verification plays a significant role to boost verification productivity by an order of magnitude by unleashing formal applications. It enables many domains in the chip design and implementation cycles including functional, safety and security verification, logic optimization at various levels of design abstractions starting from architectural levels down to implementation for both software and hardware models.

The inherit theoretical complexity of model checking presents a big barrier to scale for such complex systems. In this talk, we will show how the industry explores and exploits various techniques in model checking to make it a practical and scalable technology, including key technological and methodological inflection points that made significant innovations and managed to boost formal. We will highlight innovations and exploitation that the industry produced, including for example the concept of formal apps, democratization of formal, the concept of 100% signoff in arithmetic designs, and equivalence checking. Model checking of software is a growing interest in the chip design industry driven by the fast growth of domain specific architectures like AI and DSP chips and dedicated accelerators, where models are implemented in C++ and model checking is required.

Despite the impressive industrial advancements and successful applications of model checking technologies for chip design, the domain is still very young considering its high expected impact on the industry. Therefore, in this talk we are interested in inspiring the academic community and accelerating research in key challenges through a joint and focused research with the industry. The intent is to boost core model checking algorithms and abstraction research, as well as model checking applications in key verification areas such as cybersecurity, automotive safety, and machine learning algorithms. Recently we have observed a rising research front of quantum computing leveraging formal verification technologies which could have major impact on the scalability and applications of quantum machines. Through collaboration, the academic and industrial communities can hugely influence the pace of innovation in these critical areas.

ABSTRACT. In the recent years, the interest in combining symbolic and sub-symbolic AI approaches has been rapidly increasing. In particular neuro-symbolic AI, in which the two approaches have been combined in a number of different ways, is in the center of attention. A natural question in this context is how answer set programs, one of the main non-monotonic rule-based formalisms in use today, may fit into this endeavor. Several authors have considered how to combine answer set programs with subsymbolic AI, specifically with (deep) neural networks, at varying levels of integration in order to facilitate semantics-enhanced applications of AI that build on subsymbolic AI such as scene classification, object tracking, or visual question answering. In this talk, we shall consider hybrid answer set programming approaches and explore opportunities and challenges for them. Notably, combining answer set programs with alternative inference approaches is not novel and has been extensively studied e.g. for logic-based ontologies. We shall also revisit lessons learnt from such work for the ongoing work on hybrid answer set programming.

ABSTRACT. Dealing with context dependent knowledge has led to different formalizations of the notion of context. Among them is the Contextualized Knowledge Repository (CKR) framework, which is rooted in description logics but links on the reasoning side strongly to logic programs and Answer Set Programming (ASP) in particular. The CKR framework caters for reasoning with defeasible axioms and exceptions in contexts, which was extended to knowledge inheritance across contexts in a coverage (specificity) hierarchy. However, the approach supports only this single type of contextual relation and the reasoning procedures work only for restricted hierarchies, due to non-trivial issues with model preference under exceptions. In this paper, we overcome these limitations and present a generalization of CKR hierarchies to multiple contextual relations, along with their interpretation of defeasible axioms and preference. To support reasoning, we use ASP with algebraic measures, which is a recent extension of ASP with weighted formulas over semirings that allows one to associate quantities with interpretations depending on the truth values of propositional atoms. Notably, we show that for a relevant fragment of CKR hierarchies with multiple contextual relations, query answering can be realized efficiently with the popular asprin framework. The algebraic measures approach is more powerful and enables e.g. reasoning with epistemic queries over CKRs, which opens interesting perspectives for the use of quantitative ASP extensions in other applications. The paper has been presented at the 37th International Conference on Logic Programming (ICLP 2021).

ABSTRACT. Defeasible description logics (DDLs) support nonmonotonic reasoning by admitting defeasible concept inclusions in the knowledge base. Early reasoning methods for subsumption did not always use defeasible information for objects in the scope of nested quantifiers and thus neglected un-defeated information. The reasoning approach employing typicality models for the DDL EL_⊥ overcomes this effect for existentially quantified objects.

In this extended abstract we report on how to lift typicality model-based reasoning to the DDL ELI_⊥, which extends EL_⊥ with inverse roles. These can capture a form of universal quantification and extend expressivity of the DDL substantially. Reasoning in DDLs often employs rational closure according to the propositional KLM postulates. We can show that the proposed subsumption algorithm yields more entailments than rational propositional entailment.

ABSTRACT. In the field of non-monotonic logics, the notion of Rational Closure (RC) is acknowledged as a notable approach. In recent years, RC has gained popularity in the context of Description Logics (DLs), and in this work, we show how to integrate RC within the triple language RDFS (Resource Description Framework Schema), which together with OWL 2 is a major standard semantic web ontology language. To do so, we start from ρdf, a minimal, but significant RDFS fragment that covers the essential features of RDFS, and then extend it to ρdf⊥, allowing to state that two entities are incompatible/disjoint with each other. Eventually, we propose defeasible ρdf⊥ via a typical RC construction allowing to state default class/property inclusions. The main features of our approach are: (i) the defeasible ρdf⊥ we propose here remains syntactically a triple language by extending it with new predicate symbols with specific semantics; (ii) the logic is defined in such a way that any RDFS reasoner/store may handle the new predicates as ordinary terms if it does not want to take account of the extra non-monotonic capabilities; (iii) the defeasible entailment decision procedure is built on top of the ρdf⊥ entailment decision procedure, which in turn is an extension of the one for ρdf via some additional inference rules favouring a potential implementation;(iv) the computational complexity of deciding entailment in ρdf and ρdf⊥ are the same; and (v) defeasible entailment can be decided via a polynomial number of calls to an oracle deciding ground triple entailment in ρdf⊥ and, in particular, deciding defeasible entailment can be done in polynomial time.

ABSTRACT. The importance of taking individual, potentially conflicting perspectives into account when dealing with knowledge has been widely recognised. Many existing ontology management approaches fully merge knowledge perspectives, which may require weakening in order to maintain consistency; others represent the distinct views in an entirely detached way. As an alternative, we propose Standpoint Logic, a simple, yet versatile generic approach to extend existing KR formalisms by the capability to express domain knowledge relative to diverse, possibly conflicting standpoints, which can be hierarchically organised, combined, and put in relation with each other. As a concrete showcase, this extended abstract introduces the standpoint-enhanced version of the very expressive description logic SROIQbs, which is tightly connected to the W3C-standardised ontology language OWL 2 DL. We report that, by virtue of a “small model property” and using some elaborate encoding tricks, it is possible to establish a polytime translation from standpoint-enhanced SROIQbs into plain SROIQbs. By virtue of this result, existing highly optimised OWL reasoners can be used off the shelf to provide practical reasoning support for ontology languages from the OWL family extended by standpoint modelling.