ABSTRACT. Metis is an ordered paramodulation prover built into the Isabelle/HOL proof assistant. It attempts to close the current goal using a given list of lemmas. Typically these lemmas are found by Sledgehammer, a tool that integrates external automatic provers. We present a new tool that analyzes successful Metis proofs to derive variable instantiations. These increase Sledgehammer’s success rate, improve the speed of Sledgehammer-generated proofs, and help users understand why a goal follows from the lemmas.

ABSTRACT. Congruence closure on ground equations is a well-established and efficient algorithm for deciding ground equalities. It constructs an explicit representation of ground equivalence classes based on a given set of input equations, allowing ground equalities to be decided by membership. In many applications, these ground equations originate from grounding non-ground equations.

We propose an algorithm that directly computes a non-ground representation of ground congruence classes for non-ground equations. Our approach is sound and complete with respect to the corresponding ground congruence classes. Experimental results demonstrate that computing non-ground congruence classes often outperforms the classical ground congruence closure algorithm in efficiency.

ABSTRACT. We introduce anti-pattern templates, which extend both anti-pattern matching by abstracting ground terms to variables, and unification by negative constraints. For anti-patter templates, we study the satisfiability problem, which asks whether a given template can be instantiated to a valid anti-pattern matching instance.

We show that the satisfiability problem for anti-pattern templates is NP-complete, but it becomes tractable if the number of negation symbols is bounded. Next, we consider anti-pattern templates modulo an equational theory and discuss its relations with other variants of equational frameworks with negative constraints. In particular, we conclude that the satisfiability problem for anti-pattern templates considered modulo associativity becomes undecidable, while it is decidable modulo associativity and commutativity.

ABSTRACT. In computer science and mathematical logic, formal languages abstract away concrete syntax details, focusing on abstract syntax to capture structural properties. However, conventional abstract syntax falls short for languages with variable-binding constructs. In this paper, we work with the nominal language which is a general formal language for representing binders, freshness conditions and $\alpha$-renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs a generalisation of permutation fixed-point constraints in $\alpha$-equivalence judgements, seamlessly integrating commutativity into the reasoning process.

We investigate the proof-theoretical properties of the framework and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. Moreover, thanks to the use of fixed point constraints, the resulting unification theory is finitary, unlike the standard nominal unification modulo commutativity using freshness constraints. This extension provides a robust foundation for structural induction and recursion over syntax with binding constructs and commutative operators, such as first-order logic and the $\pi$-calculus, enabling reasoning modulo both $\alpha$-equivalence and commutativity.

ABSTRACT. In this paper, we present a practical method for computing uniform interpolation (UI) and forgetting in ELIH-ontologies, addressing fundamental operations critical for detecting semantic differences in ontology evolution. Our method extends previous work to accommodate inverse roles while maintaining termination and soundness guarantees. Empirical evaluation across industry benchmark datasets Oxford ISG and NCBO BioPortal demonstrates 100% success rates with significant improvements in computational efficiency compared to state-of-the-art systems. The practical impact of our approach is validated through application to SNOMED CT, the world's largest clinical terminology supporting healthcare information systems globally. This enables terminologists and developers to systematically track semantic differences, detect unintended consequences, and validate change safety across SNOMED CT releases.

ABSTRACT. Standard Description Logics (DLs) can encode quantitative aspects of an application domain through either *number restrictions*, which constrain the number of individuals that are in a certain relationship with an individual, or *concrete domains*, which can be used to assign concrete values to individuals using so-called features. These two mechanisms have been extended towards very expressive DLs, for which reasoning nevertheless remains decidable. Number restrictions have been generalized to more powerful comparisons of sets of role successors in ALCSCC, while the comparison of feature values of different individuals in ALC(D) has been studied in the context of ω-admissible concrete domains D. In this paper, we combine both formalisms and investigate the complexity of reasoning in the thus obtained DL ALCOSCC(D), which additionally includes the ability to refer to specific individuals by name. We show that, in spite of its high expressivity, the consistency problem for this DL is ExpTime-complete, assuming that the constraint satisfaction problem of D is also decidable in exponential time. It is thus not higher than the complexity of the basic DL ALC. At the same time, we show that many natural extensions to this DL, including a tighter integration of the concrete domain and number restrictions, lead to undecidability.

ABSTRACT. This paper introduces a proof calculus for real-analytic differential-algebraic dynamic logic, a variant of differential-algebraic dynamic logic. Our calculus allows correct reduction of differential-algebraic equations to ordinary differential equations through axiomatized index reduction. Additionally, it ensures compatibility between differential-algebraic equation proof calculus and (differential-form) differential dynamic logic for hybrid systems. One key contribution is ghost switching which establishes precise conditions to decompose multi-modal systems into hybrid pro- grams, thereby correctly hybridizing sophisticated differential-algebraic dynamics. We demonstrate our calculus on a Euclidean pendulum and formally verify its energy conservation.

ABSTRACT. Many procedures for SAT-related problems, in particular for those requiring the complete enumeration of satisfying truth assignments, rely their efficiency and effectiveness on the detection of (possibly small) partial assignments satisfying an input formula. Surprisingly, there seems to be no unique universally-agreed definition of formula satisfaction by a partial assignment in the literature. In this paper we analyze in deep the issue of satisfaction by partial assignments, highlighting some ambiguities and subtleties of this concept, and investigating their practical consequences. We identify two alternative notions that are implicitly used in the literature, namely verification and entailment, which coincide if applied to CNF formulas but differ and present complementary properties if applied to non-CNF or to existentially-quantified formulas. We show that, although the former is easier to check and as such is implicitly used by most current search procedures, the latter has better theoretical properties, and can improve the efficiency and effectiveness of enumeration procedures.

ABSTRACT. We consider the problem of finding and enumerating polyominos that can be folded into multiple non-isomorphic boxes. While several computational approaches have been explored, including SAT, randomized algorithms, and decision diagrams, none has been able to perform at scale. We argue that existing SAT encodings are hindered by the presence of global constraints (e.g., graph connectivity or acyclicity), which are generally hard to encode effectively, and hard for solvers to reason about. In this work, we propose a new SAT-based approach that replaces these global constraints with simple local constraints that have substantially better propagation properties. Our approach dramatically improves the scalability of both computing and enumerating common box unfoldings: (i) while previous approaches could only find common unfoldings of two boxes up to area 88, ours easily scales up to 150, and (ii) while previous approaches were only able to enumerate common unfoldings up to area 30, ours scales up to 60. This allows us to rule out 46, 54, and 58 as the smallest areas allowing a common unfolding of three boxes, thereby refuting a conjecture of Xu et al. (2017).