ABSTRACT. Generative Datalog is an extension of Datalog that incorporates constructs for referencing parameterized probability distributions. This augmentation transforms the evaluation of a Generative Datalog program into a stochastic process, resulting in a declarative formalism suitable for modeling and analyzing other stochastic processes. This work provides an introduction to Generative Datalog through the lens of Answer Set Programming (ASP), demonstrating how Generative Datalog can explain the output of ASP systems that include @-terms referencing probability distributions. From a theoretical point of view, extending the semantics of Generative Datalog to stable negation proved to be challenging due to the richness of ASP relative to Datalog in terms of linguistic constructs. On a more pragmatic side, the connection between the two formalisms lays the foundation for implementing Generative Datalog atop efficient ASP systems, making it a practical solution for real-world applications.

ABSTRACT. Automated planning is a prominent area of Artificial Intelligence, and an important component for intelligent autonomous agents. A critical aspect of domain-independent planning is the domain model, that encodes a formal representation of domain knowledge needed to reason upon a given problem. Despite the crucial role of domain models in automated planning, there is lack of tools supporting knowledge engineering process by comparing different versions of the models, in particular, determining and highlighting differences the models have. In this paper, we build on the notion of strong equivalence of domain models and formalise a novel concept of similarity. To measure the similarity of two models, we introduce a directed graph representation of lifted domain models that allows to formulate the domain model similarity problem as a variant of the graph edit distance problem. We propose an Answer Set Programming approach to optimally solve the domain model similarity problem, that identifies the minimum number of modifications the models need to become strongly equivalent, and we demonstrate the capabilities of the approach on a range of benchmark models.

ABSTRACT. Modern semiconductor manufacturing involves intricate production processes consisting of hundreds of operations, which can take several months from lot release to completion. The high-tech machines used in these processes are diverse, operate on individual wafers, lots, or batches in multiple stages, and necessitate product-specific setups and specialized maintenance procedures. This situation is different from traditional job-shop scheduling scenarios, which have less complex production processes and machines, and mainly focus on solving highly combinatorial but abstract scheduling problems. In this work, we address the scheduling of realistic semiconductor manufacturing processes by modeling their specific requirements using hybrid Answer Set Programming with difference logic, incorporating flexible machine processing, setup, batching and maintenance operations. Unlike existing methods that schedule semiconductor manufacturing processes locally with greedy heuristics or by independently optimizing specific machine group allocations, we examine the potentials of large-scale scheduling subject to multiple optimization objectives.

ABSTRACT. In answer set programming, two groups of rules are considered strongly equivalent if replacing one group by the other within any program does not affect the set of stable models. Jan Heuer has designed and implemented a system that verifies strong equivalence of programs in the ASP language mini-gringo. The design is based on the syntactic transformation that converts mini-gringo programs into first-order formulas. Heuer’s assertion about this translation that was supposed to justify this procedure turned out to be incorrect, and in this paper we propose an alternative justification for his algorithm. We show also that this translation can be replaced by the simpler and more natural translation and the algorithm will still produce correct results.

ABSTRACT. The Hamiltonian Cycle Reconfiguration Problem is defined as determining, for a given Hamiltonian cycle problem and two among its feasible solutions, whether one is reachable from another via a sequence of feasible solutions subject to certain transition constraints. We develop an approach to solving the Hamiltonian cycle reconfiguration problem based on Answer Set Programming (ASP). Our approach relies on a high-level ASP encoding and delegates both the grounding and solving tasks to an ASP-based solver. To show the effectiveness of our approach, we conduct experiments on the benchmark set of Flinders Hamiltonian Cycle Project.

ABSTRACT. We develop an approach called bounded combinatorial reconfiguration for solving combinatorial reconfiguration problems based on Answer Set Programming (ASP). The general task is to study the solution spaces of source combinatorial problems and to decide whether or not there are sequences of feasible solutions that have special properties. The resulting recongo solver covers all metrics of the solver track in the most recent international competition on combinatorial reconfiguration (CoRe Challenge 2022). recongo ranked first in the shortest metric of the single-engine solvers track. In this paper, we present the design and implementation of bounded combinatorial reconfiguration, and present an ASP encoding of the independent set reconfiguration problem that is one of the most studied combinatorial reconfiguration problems. Finally, we present empirical analysis considering all instances of CoRe Challenge 2022.

ABSTRACT. Approximation fixpoint theory (AFT) is a powerful framework that has been widely used for defining the semantics of non-monotonic formalisms in artificial intelligence and logic programming. In particular, AFT is used to derive the fixed points of (potetially non-monotonic) operators over complete lattices. However, in practice, there often arise operators that are defined over structures that are not necessarily complete lattices. Therefore, the quest for a more general version of AFT has been lingering as a potentially interesting research direction. We develop an extension of AFT, namely Categorical AFT, that allows us to study the fixed points of (potentially non-functorial) operators defined over appropriate categories. Since categories are more general structures than complete lattices, we argue that our approach provides a more general and unified framework for the study of non-monotonicity. The versatility of category theory creates the potential of new insights and applications.

ABSTRACT. Equilibrium logic is a logical characterization of Answer Set Programming (ASP). Guided by key challenges from the defeasible deontic logic literature we introduce Deontic Equilibrium Logic with eXplicit negation (DELX), its extension for normative reasoning. In contrast to modal approaches to deontic logic, DELX exploits a normal form that allows obligation and prohibition operators to be applied to atoms only. We prove that arbitrary theories in DELX are reducible to ASP and illustrate how this minimalist approach can handle these challenges.

ABSTRACT. In this paper, we introduce game-theoretic semantics (GTS) for Qualitative Choice Logic (QCL), which, in order to express preferences, extends classical propositional logic with an additional connective called ordered disjunction. In particular, we present a new semantics that makes use of GTS negation and, by doing so, avoids contentious behavior of negation in existing QCL-semantics.

ABSTRACT. The class of inductive inference operators that extend rational closure, as introduced by Lehmann or via Pearl’s system Z, exhibits desirable inference characteristics. The property that formalizes this, known as (RC Extension), has recently been investigated for basic defeasible entailment relations. In this paper, we explore (RC Extension) for more general classes of inference relations. First, we semantically characterize (RC Extension) for inference relations based on preferential models in general. Then we focus on operators that can be represented with strict partial orders (SPOs) on possible worlds and characterize SPO representable inductive inference operators. Furthermore, we show that for SPO representable inference operators, (RC Extension) is semantically characterized as a refinement of the Z-rank relation on possible worlds.

ABSTRACT. Some reasoning methods for Defeasible Description Logics (DDLs) suffer from quantification neglect (QN) as they omit un-defeated information for quantified objects. Reasoning in defeasible EL⊥ based on so-called typicality models (TMs), which extend canonical models of classical EL⊥, can alleviate QN. The DDL ELI⊥ extends EL⊥ by inverse roles, i.e., a limited form of value restriction. Extending TMs to inverse roles is challenging due to their interaction with existential restrictions. In this paper, we develop TMs for ELI⊥ for 4 different semantics reliant on rational and relevant closure. We show that our computation methods for those TMs are effective decision procedures for subsumption in defeasible ELI⊥ and that the stronger forms of TMs can mitigate QN.

ABSTRACT. Weighted knowledge bases for description logics with typicality under a "concept-wise" multi-preferential semantics provide a logical interpretation of MultiLayer Perceptrons. In this context, Answer Set Programming (ASP) has been shown to be suitable for addressing defeasible reasoning in the finitely many-valued case, providing a $\Pi^p_2$ upper bound on the complexity of the problem, nonetheless leaving unknown the exact complexity and only providing a proof-of-concept implementation. This paper fulfils the lack by providing a $\sc{P^{NP[log]}}$-completeness result and new ASP encodings that deal with weighted knowledge bases with large search spaces.

ABSTRACT. We detail two instantiations of a generic algorithm for the problematic and MUS-variable-based inconsistency measures, based on answer set programming and Boolean satisfiability (SAT). Empirically, the SAT-based approach allows for more efficiently computing the measures when compared to enumerating all minimal correction subsets of a knowledge base.

ABSTRACT. Partial functions are ubiquitous in Knowledge Representation applications, ranging from practical, e.g., business applications, to more abstract, e.g., mathematical and programming applications. Expressing propositions about partial functions may lead to non-denoting terms resulting in undefinedness errors and ambiguity, causing subtle modeling and reasoning problems.

In our approach, formulas are well-defined (true or false) and non-ambiguous in all structures. We develop a base extension of three-valued predicate logic, in which partial function terms are guarded by domain expressions ensuring the well-definedness property despite the three-valued nature of the underlying logic. To tackle the verbosity of this core language, we propose different ways to increase convenience by using disambiguating annotations and non-commutative connectives. We show a reduction of the logic to two-valued logic of total functions and prove that many different unnesting methods turning partial functions into graph predicates, which are not equivalence preserving in general, are equivalence preserving in the proposed language, showing that ambiguity is avoided.

ABSTRACT. We consider a description logic L over the concrete domain made of finite strings over a finite alphabet, the prefix relation and equalities to constant strings. Using an automata-based approach, we show that the concept satisfiability problem w.r.t. general TBoxes for L is EXPTIME-complete for all finite alphabets. As far as we know, this is the first complexity result for an expressive description logic with a nontrivial concrete domain on strings.

ABSTRACT. We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics. Our primary object of interest is ALCvpl, an extension of ALC with path expressions using visibly-pushdown languages, which was shown to be decidable by Löding et al. in 2007. The paper present a series of undecidability results. We prove undecidability of ALCvpl with the seemingly innocent Self operator. Then, we consider the simplest non-regular (visibly-pushdown) language r #s # := {r n s n | n ∈ N}. We establish undecidability of the concept satisfiability problem for ALCreg extended with nominals and r #s #, as well as of the query entailment problem for ALC-TBoxes, where such non-regular atoms are present in queries.