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