ABSTRACT. We show that logic-based argumentation, and in particular sequent-based frameworks, is a robust argumentative setting for abductive reasoning and explainable artificial intelligence.

ABSTRACT. In this paper, we study the effect of preferences in abstract argumentation under a claim-centric perspective. Recent work has revealed that semantical and computational properties can change when reasoning is performed on claim-level rather than on the argument-level, while under certain natural restrictions (arguments with the same claims have the same outgoing attacks) these properties are conserved. We now investigate these effects when, in addition, preferences have to be taken into account and consider four prominent reductions to handle preferences between arguments. As we shall see, these reductions give rise to different classes of claim-augmented argumentation frameworks, and behave differently in terms of semantic properties and computational complexity. This strengthens the view that the actual choice for handling preferences has to be taken with care.

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. 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.