We propose a description language capturing a simple but central aspect of the possible “lives” (the behavior) of a database application, namely the ability for the relations to grow, shrink, or keep the same size. We first consider arbitrary behaviors and investigate the basic properties of such descriptions. We characterize consistency, redundancy, and subsumption, and show that every behavior has a unique minimal complete description. We then consider the problem of computing the minimal complete description of a given database application. We model such applications as collections of procedures, specified by update programs based on relational algebra. The general problem is undecidable, even for an application consisting of a single procedure with a single update language statement. We also identify decidable cases and provide partial complexity characterisations.
Argumentation frameworks (AFs) provide a central formalism for abstract argumentation, representing arguments and their interactions as attack graphs and serving as reasoning engines across diverse domains. One of their main strengths lies in their ability to support explanations. However, their usefulness can be limited by size and structural complexity, which can hinder understanding. To address this challenge, we investigate simplification techniques for AFs, with particular emphasis on clustering-based abstraction. By grouping arguments into clusters and interpreting attacks accordingly, clustered AFs provide reduced representations that preserve essential argumentative properties while hiding redundant details. We study formal underpinnings for clustering on AFs in particular combined with other simplification techniques, and analyze their effects on main argumentation semantics, and explore conditions under which simplifications remain faithful and avoid spurious results. Our approach positions clustering as a principled method of abstraction and highlights its potential for enhancing explainability in argumentation.
We study two approximate variants of inclusion atoms and examine the axiomatization and computational complexity of their implication problems. The approximate variants allow for some imperfection in a team (corresponding to a unirelational database), and differ in how this degree is measured. One considers the error relative to the size of the team, while the other applies a fixed threshold independent of size. We obtain complete axiomatizations for both under some arity restrictions. In particular, restricted to unary atoms, the implication problem for each approximate variant is decidable in polynomial time.
In this paper we investigate splitting notions for conditional belief bases that allow us to localize reasoning and computations to only the relevant parts of a belief base. The focus of our investigations lies on splitting notions for c-representations, which are special kinds of Spohn’s ranking models for belief bases and which can be specified via a constraint satisfaction problem. We extend the notion of constraint splittings for c-representations to conditional constraint splittings, covering also cases where the subbases may share conditionals. Inspired by conditional syntax splittings, we identify the subclass of safe conditional constraint splittings, allowing us to solve the constraint systems of the subbases independently from each other. We elaborate the relationships of constraint and safe conditional constraint splittings to safe and generalized safe conditional syntax splittings and also to safe covers, which have been proposed for localized computation of c-representations. Additionally, we generalize solution splittings for c-representations to safe conditional c-solution splittings and show how they relate to conditional constraint splittings.
In this paper we bring together qualitative temporal reasoning and planning in order to pave the way for a new approach to planning and temporal planning. Both fields are concerned with arrangement problems of temporal intervals. We present a method to construct qualitative temporal reasoning tasks from planning problems, effectively reducing a class of planning tasks to qualitative temporal reasoning. The construction proposed in this paper enables additional temporal planning constraints to be considered, thereby making the method applicable to both classical planning and temporal planning.
The optimal repair property, which says that there is a finite set of optimal (i.e., entailment-maximal) repairs that covers all repairs, has turned out to be useful both in the context of ontology engineering and in belief change. We provide abstract order-theoretic conditions that guarantee the existence of finite sets of optimal repairs covering all repairs, and illustrate their use with abstract examples as well as with more practical examples from the realm of Description Logic (DL). The order-theoretic view on optimal repairs also reveals that there is a strong similarity between the optimal repair property and the existence of a finite complete set of unifiers for unification modulo equational theories. Applying Siekmann’s proposal to divide unification problems into the unification types unitary, finitary, infinitary, and zero to repair problems, we obtain a more fine-grained classification of repair problems. For the DL examples introduced in this paper, we observe that types unitary, finitary and zero can occur, but none of these examples provides us with an infinitary repair problem. However, we also show that unification problems can actually be viewed as repair problems in the abstract framework introduced in our previous work on contractions based on optimal repairs. Thus, within this framework, known results on unification types of certain equational theories provide us with examples of repair problems of these types.
Machine-learning-based algorithm selection has demonstrated improvements in SMT solving by exploiting solver complementarity across diverse problem families. Existing SMT algorithm selectors primarily rely on handcrafted syntactic features to represent problem instances for machine-learning models. In this work, we explore whether high-level natural-language descriptions of SMT instances can provide additional useful information. We present SMT-Select, an SMT algorithm selection framework that combines traditional syntactic features with semantic embeddings derived from natural-language descriptions using pretrained transformer models. It further improves upon the algorithm selection pipeline of the state-of-the-art selector MachSMT. Evaluated on SMT-COMP 2024 benchmarks across 9 logics, SMT-Select achieves improved performance in 7 logics when description-based features are added, while performance degrades in the remaining two logics, where the SMT-LIB descriptions exhibit very limited variability. To address this limitation, we outline future work on LLM-based agents for generating higher-quality SMT instance descriptions, supported by preliminary demos.
Recent research has provided a framework for measuring similarity of incomplete database instances without considering the presence of complete key information; the aim is to identify similar tuples across database instances by purely relying on the tuples themselves. The framework proposes a straight forward approach for an approximate algorithm to reach sufficiently good results with computational efficiency. Introducing more advanced methods for nearest neighbour searches, such as locality sensitive hashing (LSH), is an opportunity to build on top of the original framework and further enhance the already achieved results. Hence, this paper introduces the appropriate definitions and proves the performance of an LSH integrated framework based on extensive experiments. Further, using an LSH integrated approach broadens the application space of the framework for more types of data as well as detecting partial instance matches, which highlights how promising this approach is for future work.
The guarded fluted (forward) fragment is the intersection of the guarded fragment and the fluted (forward) fragment of first-order logic. In this paper we showcase a simple and special model construction technique which turns each first-order structure into a modal structure and back. Based on that, we devise a translation of the two guarded fragments to the basic modal logic extended with the universal modality, providing a simulation of the guarded fluted fragment as well as a new proof of the ExpTime-completeness of the satisfiability problem. Moreover, our technique induces a variant of the unraveling construction. As an application of the unraveling, we prove the Łoś-Tarski Preservation Theorem in the two fragments.
Commonsense visual sensemaking requires robust mechanisms to extract scene elements and other visual features from perceived imagery, as well as rich conceptual commonsense knowledge and reasoning to interpret the perceived interactive dynamic. In this context, we position ongoing work on using integrated Vision Language Models (VLM) and Answer Set Programming (ASP) based reasoning about (dynamic) spatial configurations using VLMs as a neural foundation for symbolic modeling of dynamic scene structures. We sketch preliminary results highlighting practical usability by application to the task of Visual Question Answering (VQA) with the STRIDE-QA driving dataset.
We show that revision by single sentences and multiple revision are, in general, mutually irreducible processes. The result is given for revision in base logics, a framework for studying revision in arbitrary classical logics for various notions of bases. Within this framework, we demonstrate that revision by single sentences can not be represented as multiple revision. The result employs general relational semantics for base revision. In combination with the well-known result that multiple revision cannot be reduced to sentence revision, we obtain that sentence revision and multiple revision are mutually irreducible.
We examine the Intermediate Knowledge Problem (IKP): the challenge of maintaining coherent, goal-aligned intermediate representations during multi-step reasoning. The issue is particularly acute in automated knowledge elicitation and engineering, where analysis relies on provisional and revisable artifacts. Using Grounded Theory as a running example, we illustrate why existing symbolic systems and large language model based pipelines provide limited support for such intermediate knowledge, identifying a central obstacle to automating knowledge elicitation and engineering methods.
Belief expansion is the operation of incorporating new information into a belief base or theory. If a belief state can draw on a set of fundamental beliefs, new pieces of information are often not simply added, but explicitly tied to fundamental beliefs by means of explanations. Abductive expansion is an AGM-style belief change operation that augments a theory with an underlying explanation by means of abduction. AGM-style belief change presupposes deductively closed theories and thus makes no distinction between the explanation and the explained. In this paper, we extend abductive expansion to belief bases, which do not presuppose deductive closure. Within bases, abduced information is introduced in response to unexplained input and can therefore be explicitly identified as a newly formed belief. We provide an axiomatic characterization along with constructive methods.
Central reasoning tasks arising in computational argumentation are NP-hard. The field of knowledge compilation studies formal representations that permit efficient reasoning, which, however, have so far not found their way into mainstream research in computational argumentation. We study how to compile parts of argumentation frameworks (AFs)—a central representation for argumentative reasoning—to binary decision diagrams (BDDs) in search-based algorithms. We show promise of compilation in an experimental evaluation of the resulting algorithms, which incorporate multiple heuristics.
The analysis of abrasive wear is central to sustainable material design and tool development, yet current practice relies on manual inspection of scanning electron microscopy (SEM) images, limiting scalability and reproducibility. We propose early work towards a neuro-symbolic approach that integrates convolutional neural networks for SEM image segmentation with an expert-elicited taxonomy of wear features encoded in Answer Set Programming. A curated dataset of 400 laboratory and field SEM images with expert-labeled annotations supports interpretable detection of wear mechanisms. This approach aims to reduce the dependency on large datasets, increase interpretability, in automated abrasive wear analysis. The contribution opens the way for scalable and transparent decision processes in tribology, with implications for efficient materials development and extended service life of industrial tools.
Simple and short query explanations that detail how a query result is obtained from an input dataset are a powerful way to gain insight into the results of queries. Unfortunately, simple and short explanations for recursive queries are non-trivial: query results of recursive queries typically have a huge set of equally-valid explanations. Toward providing simple and short query explanations, we believe that there is a strong need for an improved understanding of explanations of recursive queries. In this paper, we present such a framework by studying explanations of facts derived using Datalog derivation rules. To enable simple explanations, we present a standard tree-based formal representation of explanations and we formalize four conceptually distinct types of simple explanations based on their tree structure. Next, we show how to effectively compute two types of simple explanations, which opens the door for practical algorithms to explain Datalog query results. Finally, we prove that computing the other two types of simple explanations involves solving NP-complete decision problems and, hence, is inherently hard.
Awareness-Based Indistinguishability Logic (henceforth, AIL) is an extension of Epistemic Logic by introducing the notion of awareness, distinguishing explicit knowledge from implicit knowledge. In this framework, each of these notions is represented by a modal operator. On the other hand, HMS models, developed in the economics literature, also provide a formalization of those notions. Nevertheless, the behavior of the epistemic operators in AIL within HMS models has yet to be explored. In this paper, we define a transformation of an AIL model into an HMS model and prove that a translation between the fragments of the language of AIL preserves truth under this transformation. As a result, we clarify the semantic role of an epistemic operator in AIL, which is essential to define explicit knowledge, within HMS models. Furthermore, we demonstrate the differences in the implicit knowledge captured by AIL and HMS models. This work lays the groundwork for a comparative analysis between the model classes.
We introduce a two-sort weighted modal logic for possibilistic reasoning with fuzzy formal contexts. The syntax of the logic includes two types of weighted modal operators corresponding to classical necessity ( ) and sufficiency ( ⊟ ) modalities and its formulas are interpreted in fuzzy formal contexts based on possibility theory. We present its axiomatization that is sound with respect to the class of all fuzzy context models. In addition, both the necessity and sufficiency fragments of the logic are also individually complete with respect to the class of all fuzzy context models. We highlight the expressive power of the logic with some illustrative examples. As a formal context is the basic construct of formal concept analysis (FCA), we generalize three main notions in FCA, i.e., formal concepts, object oriented concepts, and property oriented concepts, to their corresponding c-cut concepts in fuzzy formal contexts. Then, we show that our logical language can represent all three of these generalized notions. Finally, we demonstrate the possibility of extending our logic to reasoning with multi-relational fuzzy contexts, in which the Boolean combinations of different fuzzy relations are allowed.
Fixed-parameter tractable (FPT) algorithms have been successfully applied to many intractable problems – with a focus on decision and optimization problems. Their aim is to confine the exponential explosion to some parameter, while the time complexity only depends polynomially on the instance size. In contrast, intractable enumeration problems have received comparatively little attention so far. The goal of this work is to study how FPT decision algorithms could be turned into FPT enumeration algorithms. We thus inspect several fundamental approaches for designing FPT decision or optimization algorithms and we present ideas how they can be extended to FPT enumeration algorithms.
Hemaspaandra et al. [JCSS 2010] conjectured that satisfiability for multi-modal logic restricted to the connectives XOR and 1, over frame classes T, S4, and S5, is solvable in polynomial time. We refute this for S5 frames, by proving NP-hardness.
