ABSTRACT. First-Order Logic (FOL) is a powerful formalism that naturally captures a wide range of decision and optimization problems. Over the past two decades, automated reasoning tools such as SAT and Satisfiability Modulo Theories (SMT) solvers have advanced dramatically, making logic-based approaches practical for many applications in computer science and program analysis. Today, many program analysis techniques formulate their verification tasks as logical constraints and rely on SAT or SMT solvers to reason about them automatically. In this talk, we focus on a fragment of FOL known as Constrained Horn Clauses (CHCs) and on SPACER, a state-of-the-art CHC solver. CHCs arise naturally in many verification and synthesis applications, including the discovery and verification of inductive invariants, safety verification of finite- and infinite-state systems, model checking of pushdown systems and their extensions, modular verification of distributed and parameterized systems, type inference, and many others. A key advantage of the CHC-based approach is the separation of proof methodology from proof search. Verification tasks are first encoded as CHCs through the generation of Verification Conditions (VCs), while the responsibility for solving these conditions is delegated to a CHC solver. This separation enables a single framework to support multiple proof methodologies, programming languages, and verification tasks, while maintaining high performance and scalability.

ABSTRACT. Second-order quantifier elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the saturation-based SCAN algorithm. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding a witness for the second-order quantifiers that results in a logically equivalent first-order formula. In addition, we provide a prototype implementation of the proposed method.

ABSTRACT. Signature-based abduction in description logics (DLs) seeks the weakest sufficient hypothesis, formulated over a designated signature, that together with a background ontology explains a given observation. When no informative hypothesis is expressible within the allowed signature, existing methods based on weak forgetting inevitably produce degenerate, inquiry-blocking results such as $A\sqsubseteq\bot$. We formalize \emph{definitorial abduction}, which returns a pair $\langle\mathcal{H},\mathcal{X}\rangle$: the hypothesis $\mathcal{H}$ respects the signature restriction, while a definitorial extension $\mathcal{X}$ introduces fresh concept names anchored to the original ontology through conservative definitorial axioms. Standard signature-based abduction is the special case $\mathcal{X}=\emptyset$. To realize definitorial abduction, we develop a sound, complete, and terminating Ackermann-style strong forgetting calculus for acyclic $\mathcal{ALCI}$ ontologies. The key technical contribution is the \emph{$\exists$-surfacing rule}, which resolves a fundamental incompleteness of the Ackermann framework when a concept name to be eliminated occurs under existential restrictions in both polarities. The unnamed concept names that this rule introduces are precisely the fresh symbols that definitorial abduction exploits. We implement our approach and evaluate it on 547 real-world ontologies: 20--29\% of instances require unnamed concept names, confirming the practical prevalence of cases where standard abduction degenerates; our prototype is 36\% faster on average than the only existing baseline.

ABSTRACT. We consider and extend results on basic path logic and the related ordered fragment of first-order logic, both of which originate from the functional translation of modal logic. Using saturation-based theorem proving methods, we solve uniform interpolation for the former and second-order quantifier elimination for the latter. Basic path logic is a subclass of the ∃∗ ∀∗ -fragment and has the remarkable property that binary resolution decides it. This decidability result and the consequence finding completeness of binary resolution allows us to observe that binary resolution also decides uniform interpolation and computes uniform interpolants for basic path logic. By introducing constant Skolemisation, we show that sentences of the ordered fragment can be mapped into basic path clauses, and this mapping preserves logical consequences in the ordered fragment. We characterise the search space of the SCAN algorithm on the ordered fragment by a variation of basic path logic and prove that SCAN terminates on this class, and therefore it decides second-order quantifier elimination for this class and the ordered fragment. Finally, we propose a method for extracting uniform interpolants in the ordered fragment from the output of SCAN.

ABSTRACT. We present a first draft of an algorithm to solve existential Boolean unification with predicates. The algorithm is based on Herbrand's theorem, the witness construction for quantifier-free Boolean unification and the formula instantiation problem.

ABSTRACT. In this talk, we discuss a research program aimed at establishing systematic connections among the first-order correspondents of Sahlqvist/inductive formulas/inequalities across various relational semantic settings. We will focus on modal reduction principles, and the relational settings we will discuss include crisp and many-valued Kripke frames, and crisp and many-valued polarity-based frames (aka enriched formal contexts). Building on unified correspondence theory, we will discuss a theoretical environment which makes it possible to: (a) compare and inter-relate the various frame correspondents (in different relational settings) of any given Sahlqvist modal reduction principle; (b) recognize when first-order sentences in the frame-correspondence languages of different types of relational structures encode the same “modal content”; (c) meaningfully transfer and represent well known relational properties such as reflexivity, transitivity, symmetry, seriality, confluence, density, across different semantic contexts; (d) transfer notions and results such as the van Benthem theorem and the Goldblatt-Thomason theorem across different semantic contexts. These results can be understood as a first step in a research program aimed at making correspondence theory not just (methodologically) unified, but also (effectively) parametric.

ABSTRACT. In the present paper, we develop the correspondence theory for $\GBLe$, which can be viewed as the intuitionistic counterpart of {\L}ukasiewicz logic. Our methodology follows \cite{britz2025correspondencetheorymanyvaluedmodal}. We adopt algorithmic correspondence theory method, identify the class of inductive formulas, and develop an algorithm for computing the many-valued first-order correspondents of given inductive formulas. The key step is to find the interpretations of nominals and conominals (whose interpretations are the counterparts of singletons and their complements) in $\GBLe$ which can be translated into many-valued predicate logic.

ABSTRACT. In this talk, I will discuss several proof-relevant interpolation theorems, where we do not only factor a validity or provability judgment though an interpolant formula as is traditional, but also a deduction (or program if viewed through the lenses of Curry-Howard correspondence): if π is a cut-free proof of A ⊢ B, one can find an interpolant formula I in the common vocabulary of A and B and proofs π₁, π₂ of A ⊢ I and I ⊢ B respectively such that π₁ composed with π₂ cut-reduces to π. I will refer to such results as Čubrić' interpolation, after Djordje Čubrić who first considered this kind of statements in the 90's. I will first focus on linear logic sequent calculus and refine Maehara's method to obtain a proof-relevant interpolation result where the interpolant is completely synthesised via cut-introduction. The flexibility of the approach is exploited to carry the interpolation-as-cut-introduction to classical and intuitionistic logics. While Maehara's and Čubrić' interpolation results strongly rely on the tree structure of the deduction and its cut-freeness, I will then consider the question of how one can weaken some of those assumptions and show how proof-relevant interpolation naturally leads us to consider the interpolation problem for proofs with cuts as well as for LL proof-nets.

ABSTRACT. Formal explainability of neural network classifiers increasingly relies on logical reasoning to obtain guarantees about model behaviour in regions of the continuous input space, not just at isolated sample points. Existing formal XAI techniques often yield explanations that constrain each feature independently and therefore cannot capture the rich dependencies among features that underlie non-trivial decision boundaries. This limitation leads to explanations that are either too weak to be informative or too local to provide insight beyond the queried sample. This work introduces space explanations, a logic-based notion of explanation that represents sufficient conditions for a neural network to predict a given class over a (potentially large and geometrically complex) subset of the feature space. A space explanation is a logical formula that is sound with respect to the classifier: every point satisfying the formula is guaranteed to be classified into the target class. Due to the generality of space explanations, they can approximate non-linear decision boundaries and express relationships among features. To automatically generate space explanations, we leverage a range of flexible Craig interpolation algorithms and unsatisfiable core generation. The framework supports several strategies that expose different uses of interpolation and unsatisfiable cores. A Generalize strategy computes interpolants using families of arithmetic interpolation algorithms. A Reduce strategy weakens and simplifies explanations by computing unsatisfiable cores; A Capture strategy focuses generalization on a chosen subset of features, keeping the remaining dimensions fixed and thereby isolating interpretable relationships between selected features while still leveraging interpolation for sound generalization. These strategies are implemented in the prototype tool SpEXplAIn, focusing on QF_LRA logic, on top of the interpolating solver OpenSMT2, and integrates multiple interpolation algorithms. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the interpolation-based explanations are more meaningful than those computed by state-of-the-art.