References

1. Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Combining proofs for description logic and concrete domain reasoning. In: Fensel, A., Ozaki, A., Roman, D., Soylu, A. (eds.) RuleML+RR 2023. LNCS, vol. 14244, pp. 54–69. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-45072-3_4

2. Baader, F., Borgwardt, S., Lippmann, M.: Query rewriting for DL-lite with *n*-ary concrete domains. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI), pp. 786–792 (2017). https://doi.org/10.24963/IJCAI.2017/109

3. Baader, F., Bortoli, F.D.: The abstract expressive power of first-order and description logics with concrete domains. In: Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing (SAC), pp. 754–761 (2024). https://doi.org/10.1145/3605098.3635984

4. Baader, F., Brandt, S., Lutz, C.: Pushing the *EL* envelope. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI), pp. 364–369 (2005). http://ijcai.org/Proceedings/05/Papers/0372.pdf

5. Baader, F., Brandt, S., Lutz, C.: Pushing the *EL* envelope further. In: Proceedings of the 4th OWLED Workshop on OWL: Experiences and Directions. CEUR Workshop Proceedings (2008). https://ceur-ws.org/Vol-496/owled2008dc%5C_paper%5C_3.pdf

6. Baader, F., De Bortoli, F.: Logics with concrete domains: first-order properties, abstract expressive power, and (un)decidability. SIGAPP Appl. Comput. Rev. 24(3), 5–17 (2024). https://doi.org/10.1145/3699839.3699840

7. Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI), pp. 452–457 (1991). http://ijcai.org/Proceedings/91-1/Papers/070.pdf

8. Baader, F., Koopmann, P., Kriegel, F., Nuradiansyah, A.: Computing optimal repairs of quantified ABoxes w.r.t. static *EL* TBoxes. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 309–326. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_18

9. Baader, F., Kriegel, F.: Pushing optimal ABox repair from *EL* towards more expressive Horn-DLs. In: Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 22–32 (2022). https://doi.org/10.24963/kr.2022/3

10. Baader, F., Küsters, R.: Unification in a description logic with transitive closure of roles. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 217–232. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45653-8_15

11. Baader, F., Rydval, J.: An algebraic view on p-admissible concrete domains for lightweight description logics. In: Faber, W., Friedrich, G., Gebser, M., Morak, M. (eds.) JELIA 2021. LNCS (LNAI), vol. 12678, pp. 194–209. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-75775-5_14

12. Baader, F., Rydval, J.: Description logics with concrete domains and general concept inclusions revisited. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 413–431. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51074-9_24

13. Baader, F., Rydval, J.: Using model theory to find decidable and tractable description logics with concrete domains. J. Autom. Reason. 66(3), 357–407 (2022). https://doi.org/10.1007/S10817-022-09626-2
14. Baader, F., Sattler, U.: Description logics with aggregates and concrete domains. Inf. Syst. **28**(8), 979–1004 (2003). https://doi.org/10.1016/S0306-4379(03)00003-6

15. Baget, J., Leclère, M., Mugnier, M., Salvat, E.: Extending decidable cases for rules with existential variables. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI), pp. 677–682 (2009). http://ijcai.org/Proceedings/09/Papers/118.pdf

16. Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 457–468 (2013). See also [29] and [17]. https://doi.org/10.1145/2429069.2429124

17. Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun. ACM **58**(2), 87–95 (2015). https://doi.org/10.1145/2713167

18. Borgwardt, S., Bortoli, F.D., Koopmann, P.: The precise complexity of reasoning in *ALC* with *ω*-admissible concrete domains. In: Proceedings of the 37th International Workshop on Description Logics (DL). CEUR Workshop Proceedings (2024). https://ceur-ws.org/Vol-3739/paper-1.pdf

19. Brüggemann-Klein, A., Wood, D.: One-unambiguous regular languages. Inf. Comput. **140**(2), 229–253 (1998). https://doi.org/10.1006/INCO.1997.2688

20. Carapelle, C., Turhan, A.: Description logics reasoning w.r.t. general TBoxes is decidable for concrete domains with the EHD-property. In: Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI). Frontiers in Artificial Intelligence and Applications, pp. 1440–1448 (2016). https://doi.org/10.3233/978-1-61499-672-9-1440

21. Chandra, A.K., Merlin, P.M.: Optimal implementation of conjunctive queries in relational data bases. In: Proceedings of the 9th Annual ACM Symposium on Theory of Computing (STOC), pp. 77–90 (1977). https://doi.org/10.1145/800105.803397

22. Chekuri, C., Rajaraman, A.: Conjunctive query containment revisited. In: Afrati, F., Kolaitis, P. (eds.) ICDT 1997. LNCS, vol. 1186, pp. 56–70. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-62222-5_36

23. Cocke, J.: Programming languages and their compilers: preliminary notes, USA (1969)

24. Greiner, G., Hormann, K.: Efficient clipping of arbitrary polygons. ACM Trans. Graph. **17**(2), 71–83 (1998). https://doi.org/10.1145/274363.274364

25. Gruber, H., Holzer, M.: Finite automata, digraph connectivity, and regular expression size. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdótir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 39–50. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70583-3_4

26. Haarslev, V., Lutz, C., Möller, R.: A description logic with concrete domains and a role-forming predicate operator. J. Log. Comput. **9**(3), 351–384 (1999). https://doi.org/10.1093/LOGCOM/9.3.351

27. Haarslev, V., Möller, R., Wessel, M.: The description logic *ALC*<sub>*NH<sub>R+</sub>*</sub> extended with concrete domains: a practically motivated approach. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 29–44. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45744-5_4

28. Hales, T.C.: The Jordan curve theorem, formally and informally. Am. Math. Mon. **114**(10), 882–894 (2007). http://www.jstor.org/stable/27642361

29. Henzinger, T.A., Raskin, J.: The equivalence problem for finite automata: technical perspective. Commun. ACM **58**(2), 86 (2015). https://doi.org/10.1145/2701001
30. Hickey, T.J., Ju, Q., van Emden, M.H.: Interval arithmetic: from principles to implementation. 48(5), 1038–1068 (2001). https://doi.org/10.1145/502102.502106

31. Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Technical report, TR71-114, Cornell University (1971). https://hdl.handle.net/1813/5958

32. Hovland, D.: The inclusion problem for regular expressions. J. Comput. Syst. Sci. 78(6), 1795–1813 (2012). https://doi.org/10.1016/J.JCSS.2011.12.003

33. Jiang, S., Song, Z., Weinstein, O., Zhang, H.: A faster algorithm for solving general LPs. In: Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing (STOC), pp. 823–832 (2021). https://doi.org/10.1145/3406325.3451058

34. Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11(1), 68–85 (1975). See also [34]. https://doi.org/10.1016/S0022-0000(77)80009-3

35. Jones, N.D.: Space-Bounded Reducibility among Combinatorial Problems. J. Comput. Syst. Sci. 11(1), 68–85 (1975). See also [34]. https://doi.org/10.1016/S0022-0000(75)80050-X

36. Jordan, C.: Cours d'analyse de l'École Polytechnique—Volume 3: Calcul intégral, équations différentielles, Paris (1887). https://doi.org/10.1017/CBO9781107300064

37. Karakostas, G., Lipton, R.J., Viglas, A.: On the complexity of intersecting finite state automata and NL versus NP. Theoret. Comput. Sci. 302(1–3), 257–274 (2003). https://doi.org/10.1016/S0304-3975(02)00830-7

38. Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W., Bohlinger, J.D. (eds.) Complexity of Computer Computations. The IBM Research Symposia Series, pp. 85–103. Springer, Boston (1972). https://doi.org/10.1007/978-1-4684-2001-2_9

39. Kasami, T.: An Efficient Recognition and Syntax-Analysis Algorithm for Context-Free Languages. Report R-257, Coordinated Science Laboratory, University of Illinois, Urbana, Illinois (1966). https://doi.org/10.1007/978-1-4684-2001-2_9

40. Kazakov, Y., Klinov, P.: Advancing ELK: not only performance matters. In: Proceedings of the 28th International Workshop on Description Logics (DL). CEUR Workshop Proceedings (2015). http://hdl.handle.net/2142/74304

41. Kazakov, Y., Krötzsch, M., Simančík, F.: Practical reasoning with nominals in the *EL* family of description logics. In: Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR) (2012). https://ceur-ws.org/Vol-1350/paper-27.pdf

42. Kazakov, Y., Krötzsch, M., Simančík, F.: The incredible ELK - from polynomial procedures to efficient reasoning with *EL* ontologies. J. Autom. Reason. 53(1), 1–61 (2014). https://doi.org/10.1007/S10817-013-9296-3

43. Kozen, D.: Lower bounds for natural proof systems. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 254–266 (1977). https://doi.org/10.1109/SFCS.1977.16

44. Kriegel, F.: Beyond optimal: interactive identification of better-than-optimal repairs. In: Proceedings of the 40th ACM/SIGAPP Symposium on Applied Computing (SAC), pp. 1019–1026 (2025). https://doi.org/10.1145/3672608.3707750

45. Kriegel, F.: Optimal fixed-premise repairs of *EL* TBoxes. In: Bergmann, R., Malburg, L., Rodermund, S.C., Timm, I.J. (eds.) KI 2022. LNCS, vol. 13404, pp. 115–130. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-15791-2_11
46. Kriegel, F.: Reasoning in OWL 2 EL with Hierarchical Concrete Domains (Extended Version). LTCS-Report 25-04, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden (2025). https://doi.org/10.25368/2025.127

47. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexities of Horn description logics. ACM Trans. Comput. Logic 14(1), 2:1–2:36 (2013). https://doi.org/10.1145/2422085.2422087

48. Losemann, K., Martens, W., Niewerth, M.: Closure properties and descriptional complexity of deterministic regular expressions. Theoret. Comput. Sci. 627, 54–70 (2016). https://doi.org/10.1016/J.TCS.2016.02.027

49. Lutz, C.: NEXPTIME-complete description logics with concrete domains. ACM Trans. Comput. Log. 5(4), 669–705 (2004). https://doi.org/10.1145/1024922.1024925

50. Lutz, C.: The complexity of description logics with concrete domains. Doctoral thesis, RWTH Aachen University, Germany (2002). https://doi.org/10.1145/1024922.1024925

51. Lutz, C., Areces, C., Horrocks, I., Sattler, U.: Keys, nominals, and concrete domains. J. Artif. Intell. Res. 23, 667–726 (2005). https://doi.org/10.1613/JAIR.1542

52. Lutz, C., Miličić, M.: A tableau algorithm for description logics with concrete domains and general TBoxes. J. Autom. Reason. 38(1–3), 227–259 (2007). https://doi.org/10.1007/S10817-006-9049-7

53. Magka, D., Kazakov, Y., Horrocks, I.: Tractable extensions of the description logic EL with numerical datatypes. J. Autom. Reason. 47(4), 427–450 (2011). https://doi.org/10.1007/S10817-011-9235-0

54. Martínez, F., Ogáyar, C.J., Jiménez, J., Ruiz, A.J.R.: A simple algorithm for Boolean operations on polygons. Adv. Eng. Softw. 64, 11–19 (2013). https://doi.org/10.1016/J.ADVENGSOFT.2013.04.004

55. McNulty, G.F.: Fragments of first order logic, I: universal Horn logic. J. Symb. Log. 42(2), 221–237 (1977). https://doi.org/10.2307/2272123

56. O'Rourke, J., Chien, C., Olson, T., Naddor, D.: A new linear algorithm for intersecting convex polygons. Comput. Graph. Image Process. 19(4), 384–391 (1982). https://doi.org/10.1016/0146-664X(82)90023-5

57. Ortiz, M., Rudolph, S., Šimkus, M.: Worst-case optimal reasoning for the Horn-DL fragments of OWL 1 and 2. In: Proceedings of the 12th International Conference on Principles of Knowledge Representation and Reasoning (KR) (2010). http://aaai.org/ocs/index.php/KR/KR2010/paper/view/1296

58. Pan, J.Z., Horrocks, I.: Reasoning in the SHOQ(Dₙ) description logic. In: Proceedings of the 15th International Workshop on Description Logics (DL). CEUR Workshop Proceedings (2002). https://ceur-ws.org/Vol-53/Pan-Horrocks-shoqdn-2002.ps

59. Rydval, J.: Using model theory to find decidable and tractable description logics with concrete domains. Doctoral thesis, Dresden University of Technology, Germany (2022). https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-799074

60. Shamos, M.I.: Computational geometry. Ph.D. thesis, Yale University, United States (1978). http://euro.ecom.cmu.edu/people/faculty/mshamos/1978ShamosThesis.pdf

61. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC), pp. 1–9 (1973). https://doi.org/10.1145/800125.804029
62. Toussaint, G.T.: A simple linear algorithm for intersecting convex polygons. Vis. Comput. **1**(2), 118–123 (1985). https://doi.org/10.1007/BF01898355

63. Vatti, B.R.: A generic solution to polygon clipping. Commun. ACM **35**(7), 56–63 (1992). https://doi.org/10.1145/129902.129906

64. Younger, D.H.: Recognition and parsing of context-free languages in time $n^3$. Inf. Control **10**(2), 189–208 (1967). https://doi.org/10.1016/S0019-9958(67)80007-X

65. Yu, S., Zhuang, Q., Salomaa, K.: The state complexities of some basic operations on regular languages. Theoret. Comput. Sci. **125**(2), 315–328 (1994). https://doi.org/10.1016/0304-3975(92)00011-F

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Beyond Classical Logic
# An Analytic Representation of the Semantics of First-Order S5

Matthias Baaz<fnref n="1" /> Ⓒ, Mariami Gamsakhurdia<fnref n="1" /> Ⓒ, and Anela Lolić<fnref n="2" />✉ Ⓒ

**Abstract.** One of the most fascinating examples of the failure of Beth's definability theorem and, consequently, of Craig's interpolation theorem, is quantified S5. In this paper, we intend to establish the interpolation property for fragments of quantified S5 using a formulation of the semantics of quantified S5 as an analytic calculus in its own right. This is especially straightforward for S5, because necessity (possibility) in S5 means for all worlds (there exists a world), and we have simply to extend every predicate by a world position (worlds and objects are to be considered as separate entities).

**Keywords:** Modal S5 · Interpolation · Two-sorted logic · Herbrand's theorem · Cut elimination · Prenex fragment

## 1 Introduction

Since Craig's seminal result on interpolation [6], interpolation has been recognized as a fundamental property of logical systems. Craig interpolation has wide-ranging applications across mathematics and computer science, including consistency proofs, model checking [21], and reasoning within modular specifications and ontologies. A logic $L$ has interpolation if whenever $A \supset B$ holds in $L$ there exists a formula $I$ in the common language of $A$ and $B$ such that $A \supset I$ and $I \supset B$ both hold in $L$.

In propositional logic, interpolation properties can often be determined and classified using the foundational work of Maksimova cf. [15–17], which relies on algebraic methods. However, establishing interpolation in first-order logics is

<footnote n="1">¹ Institute of Discrete Mathematics and Geometry, TU Wien, Vienna, Austria
{baaz,mariami}@logic.at</footnote>

<footnote n="2">² Institute of Logic and Computation, TU Wien, Vienna, Austria
anela@logic.at</footnote>

<footnote>M. Baaz—This research was funded in part by the Austrian Science Fund (FWF) 10.55776/P36571.</footnote>

<footnote>M. Gamsakhurdia—This research was funded in part by the Austrian Science Fund (FWF) 10.55776/P36571.</footnote>

<footnote>A. Lolić—Recipient of an APART-MINT Fellowship of the Austrian Academy of Sciences at the Institute of Logic and Computation of TU Wien. This research was funded in part by the Austrian Science Fund (FWF) 10.55776/I5848.</footnote>
significantly more challenging, even in systems where the propositional case is
well understood.

A particularly intriguing example of the failure of interpolation (and of Beth's
definability theorem) arises in quantified modal logic, especially quantified S5.
In this paper, we explore the interpolation property for certain fragments of
quantified S5. Our approach is based on a formulation of its semantics as an
analytic calculus. This is particularly straightforward in the case of S5, where
necessity and possibility are interpreted as quantification over all worlds or the
existence of some world, respectively. We have simply to extend every predicate
by a world position.

## 2 Quantified S5

In this section we will introduce the quantified version of the modal system S5. We will not use the equality symbol [2,3]. The syntax for the basic first-order modal logic is obtained simply by taking the syntax of classical first-order logic and adding the modal operator $\Box$. Just as in classical logic, a set of predicate symbols is given which we will denote using the metavariables $P, Q, R, \dots$. For simplicity, we will not consider functions or individual constants. From a model-theoretic perspective, constants are just variables that are not being quantified. Function symbols can be modeled using predicate symbols. Thus, all terms in our modal language will be variables. We will refer to the language of quantified modal logic described here as *QML*. Now we will proceed to define formulas, models, and the satisfaction relation for first-order modal formulas.

**Definition 1.** We define formulas in quantified modal logic in the following way:

1. Any propositional symbol is a formula.

2. For any predicate symbol $P$ of arity $n$, the expression $P(x_1, \dots, x_n)$ is a formula.

3. The logical symbols $\top$ and $\bot$ are formulas.

4. If $A$ and $B$ are formulas, then $\neg A$, $A \wedge B$, $A \vee B$, and $A \supset B$ are formulas.

5. If $A$ is a formula, $\forall x A(x)$ and $\Box A$ are formulas. We write $\exists x A(x)$ as an abbreviation for $\neg \forall x \neg A(x)$, and $\diamond A$ as an abbreviation for $\neg \Box \neg A$.

In the semantic framework for quantified modal logic adopted in this paper,
variables are interpreted rigidly. That is, each variable designates the same object
across all possible worlds. As a result, it is unnecessary to specify a separate
domain of individuals for each world when defining a model. However, while
terms refer rigidly, predicate interpretations may vary from world to world, their
extensions are world-dependent.

Another important semantic choice concerns the domains over which quan-
tifiers range. In this paper, we adopt *constant domain* quantified modal logic
(see [1,8]), meaning that a single domain of quantification *D* is fixed and shared
across all possible worlds in the model.
**Definition 2.** A constant domain model $M$ based on a Kripke frame $F = (W, R)$ is a tuple $(W, R, D, V)$, where

1. $W$ is a non-empty set of possible worlds,

2. $R \subseteq W \times W$ is a binary accessibility relation on $W$ that is an equivalence relation (reflexive, symmetric, transitive).

3. $D$ is a non-empty set of individuals referred to as a domain of quantification. For each $w \in W$, $D_w = D$ (so $D_w$ is the same at each world—constant domains).

4. $V$ is a valuation function mapping each n-place predicate symbol $P$ to a subset $V(P) \subset W \times D^n$ depending on the world $w \in W$.

**Definition 3.** A variable assignment is a function usually referred to as a or b that assigns an element of the domain $D$ to each variable for a constant domain model $M = (W, R, D, V)$.

The modal logic thus models truth at a specific world. The satisfaction relation is defined as usual with the following definitions for the predicates and quantifiers, where $a$ is a variable assignment:

<table><tr><td>(M, w) |= p</td><td>iff</td><td>w ∈ V(p)</td></tr><tr><td>(M, w) |= T</td><td></td><td>always</td></tr><tr><td>(M, w) |= ⊥</td><td></td><td>never</td></tr><tr><td>(M, w) |= ¬φ</td><td>iff</td><td>(M, w) |= φ</td></tr><tr><td>(M, w) |= φ ∧ ψ</td><td>iff</td><td>(M, w) |= φ and (M, w) |= ψ</td></tr><tr><td>(M, w) |= □φ</td><td>iff</td><td>for all v ∈ W with R(w, v) we have M, v |= φ</td></tr><tr><td>(M, w) |= ◇φ</td><td>iff</td><td>there is some v ∈ W such that R(w, v) holds and M, v |= φ</td></tr><tr><td>(M, w) |= P(x<sub>1</sub>, ..., x<sub>n</sub>)[a]</td><td>iff</td><td>(w, a(x<sub>1</sub>), ..., a(x<sub>n</sub>)) ∈ V(P)</td></tr><tr><td>(M, w) |= ∀xφ[a]</td><td>iff</td><td>(M, w) |= φ[b] for every assignment b that differs from a at most on x</td></tr><tr><td>(M, w) |= ∃xφ[a]</td><td>iff</td><td>(M, w) |= φ[b] for some assignment b that differs from a at most on x</td></tr></table>

Furthermore, we can already observe from the satisfaction definition that the modal operators, □ and ◇, can be seen as an encoding of quantification over the worlds that are accessible via $R$ in a variable-free notation. This will become more apparent with the standard translation that we will present later, which transforms modal formulas to formulas in two-sorted classical first-order logic.

Note that models satisfying the equivalence of □∀xφ and ∀x□φ are constant domain models (see [1]). The following results are well-known (see [8, 13]).

**Theorem 1.** The given semantics is sound and complete for the calculus for quantified S5 for the accessibility relation being symmetric ($A \supset \Box \Diamond A$), reflexive ($\Box A \supset A$), and transitive ($\Box A \supset \Box \Box A$).
**Corollary 1.** As the accessibility relation is symmetric, reflexive, and transitive, □ can be interpreted as universal quantifier over the worlds, and ♦ can be interpreted as existential quantifier over the worlds.

Thus, models in S5 are exactly those which have an equivalence relation as world relation R. We assume without loss of generality that there only is one equivalence class of worlds. Consequently, we have that $R = W \times W$. In light of this relationship, we refer to these kinds of models as S5-models.

The following formulas are valid in S5 (see [18], p. 113):

$$ \Box \Box A = \Box A $$

$$ \Diamond \Box A = \Box A $$

$$ \Diamond \Diamond A = \Diamond A $$

$$ \Box \Diamond A = \Diamond A $$

and can also be deduced semantically, as they follow from the simple fact that in S5-models all worlds are connected to another. From this we can see that if we have several modal operators at the beginning of a propositional S5-formula, only the innermost operator is relevant for the formula's meaning.

One of the most important consequences of the cut-elimination theorem is the interpolation theorem. Recall that

**Definition 4.** A logic L admits interpolation if whenever $A \supset B$ holds in L, there is a formula I (called the interpolant) in the common language<fnref n="1" /> of A and B such that $A \supset I$ and $I \supset B$ both hold in L.

Craig proved interpolation as a lemma in order to prove Beth's definability theorem, which states that every implicitly definable symbol is also explicitly definable. In our setting, we consider a version of Beth's definability theorem specifically for individual constants, like in [7].

**Proposition 1.** *Craig's interpolation theorem implies Beth's definability theorem for constants.*

However, both, Craig's interpolation theorem and Beth's definability theorem fail for quantified S5, as was shown in Kit Fine's famous counterexample [7].

Fine's counterexample is constructed semantically via varying-domain Kripke models, but the failure persists even in constant domain models. The implicit definability fails to yield an explicit definition, and the induced failure of interpolation follows. We do not reproduce the full proof here due to its complexity. A semantic version can be found in [7], and syntactic reformulations have been discussed in later literature (e.g., [9, 11]).

**Theorem 2.** *Beth's definability theorem and consequently the Craig interpolation lemma fail for quantified S5 with constant domain.*

*Proof (Sketch).* Let T be the theory that we get if we add the following two axioms to S5:

<footnote n="1">¹ Note that the language considered in this paper is function-free.</footnote>
1. $p \supset \Diamond \forall x (F(x) \supset \Box (p \supset \neg F(x)))$,

2. $\neg p \supset \Box \exists (F(x) \wedge \Box (\neg p \supset F(x)))$.

It is shown in [7] that $p$ is implicitly definable in $T$, but not explicitly definable.

For sequent calculi, usually Craig's interpolation theorem follows by proving Maehara's lemma [20]. There are propositional sequent calculi for S5 [5], but none of them can be extended analytically to a first-order calculus such that Craig's interpolation theorem, or Maehara's lemma holds. Although analytic sequent calculi exist for propositional S5 (see, e.g., [4, 5]), no comparable system is currently known for quantified modal S5 that supports both full cut-elimination and the interpolation property as captured by Maehara's lemma. In many proof-theoretic frameworks, certain sequents - such as $A \to \Box \Diamond A$ - cannot be derived without the use of the cut rule. Moreover, Kit Fine's well-known counterexample demonstrates that both Craig's interpolation theorem and Beth's definability theorem fails in quantified S5. Any proof system validating Maehara's lemma in this setting would therefore contradict these established results.

For this reason, we adopt a purely semantic approach based on a two-sorted logic. This motivates the development of alternative proof-theoretic tools, such as the two-sorted translation and the mid-sequent interpolation techniques introduced in this paper.

## 3 Two-Sorted Logic $\mathcal{SL}$

The use of a two-sorted logic framework means that the language distinguishes between two types of variables and individual constants: those of the world sort and those of the domain sort (for individuals). Two-sorted logic can be viewed as a fragment of classical first-order logic. Formulas in this framework can be embedded into standard first-order logic by introducing additional predicates to indicate whether a variable should be of the sort world or the sort domain. In this paper, we follow the definition of two-sorted logic and the standard translation as presented in [19].

We begin by defining the language $\mathcal{SL}$ for two-sorted logic. Variables such as $x, y, z, \dots$ are used for the domain sort, while $u, v, w, \dots$ are used for the world sort. These two sets of variables are countably infinite and disjoint. Predicate symbols $P', Q', R', \dots$ correspond to those in modal first-order logic. Specifically, if $P$ is an $n$-ary predicate in the modal language, then $P'$ is an $(n+1)$-ary predicate in two-sorted logic, with the additional argument indicating the world. Thus, $P'$ is interpreted as a relation of type $\mathit{world} \times \mathit{domain}^n$. Again, the language contains no function symbols or constants. The syntax of formulas in $\mathcal{SL}$ is defined as follows:

**Definition 5.** We define formulas in two-sorted modal logic as:

1. Atomic formulas $P'(v, x_1, \dots, x_n)$ for a predicate symbol $P'$ of sort world $\times \mathit{domain}^n$, and the atomic formula $\top$ and $\bot$ are formulas.<fnref n="2" />

<footnote n="2">² No propositional constants (i.e., no atoms without world-variable arguments) are allowed, because otherwise their truth would not be world-dependent.</footnote>
2. If $\varphi$ and $\psi$ are formulas, then $\neg\varphi$, $\varphi \wedge \psi$, $\varphi \vee \psi$ and $\varphi \supset \psi$ are formulas.

3. If $\varphi$ is a formula, $a$ a free variable of domain sort and $x$ a domain variable not occurring in $\varphi$, then the expressions $\forall x\varphi'$ and $\exists x\varphi'$ are formulas, where $\varphi'$ is obtained from $\varphi$ by replacing each occurrence of $a$ in $\varphi$ by $x$.

4. If $\varphi$ is a formula, $b$ a free variable of world sort and $v$ a world variable not occurring in $\varphi$, then the expressions $\forall v\varphi'$ and $\exists v\varphi'$ are formulas, where $\varphi'$ is obtained from $\varphi$ by replacing each occurrence of $b$ in $\varphi$ by $v$.

Now we are ready to give the definition of a model in $\mathcal{SL}$.

**Definition 6.** An $\mathcal{SL}$-model is a triple $M = (W, D, V)$, where

1. $W$ and $D$ are non-empty disjoint sets,

2. $V$ is a function mapping each $(n+1)$-place predicate symbol $P'$ to a subset $V(P') \subset W \times D^n$.

**Definition 7.** An assignment in an $\mathcal{SL}$-model $M$ is a function $\mathfrak{a} = \mathfrak{a}_1 \cup \mathfrak{a}_2$, where $\mathfrak{a}_1$ maps every domain variable $x$ to an element $\mathfrak{a}_1(x) \in D$ and $\mathfrak{a}_2$ maps every world variable $u$ to an element $\mathfrak{a}_2(u) \in W$.

The satisfaction relation $M \models \varphi[\mathfrak{a}]$ for two-sorted logic is defined in the usual way:

- $M \models P'(u, x_1, \dots, x_n)[\mathfrak{a}]$ iff $(\mathfrak{a}_2(u), \mathfrak{a}_1(x_1), \dots, \mathfrak{a}_1(x_n)) \in V(P')$,

- $M \models \forall u \varphi[\mathfrak{a}]$ iff $M \models \varphi[\mathfrak{b}]$ for every assignment $\mathfrak{b}$ that differs from $\mathfrak{a}$ at most on $v$,

- $M \models \forall x \varphi[\mathfrak{a}]$ iff $M \models \varphi[\mathfrak{b}]$ for every assignment $\mathfrak{b}$ that differs from $\mathfrak{a}$ at most on $x$,

- $M \models \top(v)[\mathfrak{a}]$ always holds,

- $M \models \bot(v)[\mathfrak{a}]$ never holds,

and the standard satisfaction definitions apply to the booleans.

This completes the definition of the two-sorted logic $\mathcal{SL}$. In the next section, we define a translation from formulas of quantified modal logic S5 into $\mathcal{SL}$.

# 4 The Standard Translation to $\mathcal{SL}$

We now define a standard translation of formulas from quantified modal logic S5 into the two-sorted logic $\mathcal{SL}$. This translation preserves validity and serves as the semantic foundation for our analysis of interpolation.

The central idea is to translate modal formulas into $\mathcal{SL}$, where their logical properties can be analyzed. In particular, key results, such as the cut-elimination theorem, Maehara's lemma, and Craig's interpolation theorem hold within $\mathcal{SL}$. As a result, interpolation properties in $\mathcal{SL}$ can be leveraged to study interpolation in the original modal framework, making the translation a powerful tool.

The standard translation shows that first-order and propositional modal logic are a fragment of classical first-order logic. When reduced to propositional modal
logic, we can see that this logic is simply a variable-free notation for a fragment of first-order logic [2].

Embedding the language of quantified modal logic QML into the two-sorted language SL is straightforward. As previously discussed, each modal predicate symbol P is associated with a corresponding two-sorted predicate symbol P', where P' adds a world argument to reflect the modal structure.

**Definition 8.** Given a world variable v, we define the standard translation ST_v from QML into SL as:

$$
\begin{align*}
ST_v(P(x_1, \dots, x_n)) &= P'(v, x_1, \dots, x_n) \\
ST_v(\top) &= \top \\
ST_v(\bot) &= \bot \\
ST_v(\varphi \land \psi) &= ST_v(\varphi) \land ST_v(\psi) \\
ST_v(\neg \varphi) &= \neg ST_v(\varphi) \\
ST_v(\forall x \varphi) &= \forall x ST_v(\varphi) \\
ST_v(\Box \varphi) &= \forall w ST_w(\varphi)
\end{align*}
$$

where w is some fresh world variable.

Usually the two-sorted language and the standard translation also include and consider a predicate symbol *R* for the accessibility relation *R* on the worlds *W*. Since we will only translate formulas in the logic S5 in this work, where we have that *R* = *W* × *W* for every model, we can omit *R*. As all worlds are connected to all worlds and we work with constant domains, it consequently does not matter from which world variable *v* we start the translation *ST*<sub>*v*</sub> if every subformula is in the scope of some modal operator.

It is important to note that the significance of the standard translation lies not in the syntactic form of the resulting formula, but in its *equivalence class*. Many formulas arising in proof constructions (such as interpolants) may not be direct translations of modal formulas but are nevertheless *equivalent* to such translations. This equivalence ensures that the modal meaning is preserved.

**Definition 9.** Let $M = (W, D, V)$ be some $SL$-model and $a = a_1 \cup a_2$ an assignment in $M$. Further, let $N = (W', R, D', V')$ be an $S5$-model and $b$ be an assignment in $N$ such that $W = W'$, $D = D'$, $b = a_1$ and such that for any modal predicate symbol $P$ and counterpart $P'$ in the two-sorted language we have that $V(P) = V'(P')$. Then we call $(M, a)$ and $(N, b)$ equivalent, writing $(M, a) \sim (N, b)$.

Note that for each tuple $(M, a)$ we can find a unique equivalent tuple $(N, b)$. Now that we have defined the standard translation, the question arises whether the translation of a formula that is valid in constant-domain S5 is still valid in $SL$.

**Lemma 1.** Suppose that we have two equivalent models $(M, a) \sim (N, b)$. For every formula $\varphi$ in quantified modal logic and a world variable $v$ we have that

$$(N, a(v)) \models \varphi[b] \text{ iff } M \models ST_v(\varphi)[a].$$
*Proof.* Straightforward by induction on the structure of the formula $\varphi$.

Thus, the standard translation is validity preserving. We can also map the S5-models to models in two-sorted logic bijectively such that we can use them interchangeably: $M = (W, R, D, V) \mapsto N = (W, D, V)$.

We can further argue that valid S5 sentences remain valid under translation to $\mathcal{SL}$ by demonstrating that the translations of all axioms and inference rules of constant domain S5 can be derived within $\mathcal{SL}$ using Gentzen's sequent calculus. For example, we can derive the translation of the axiom $\Box A \supset \Box\Box A$, which is $\forall vA'(v) \supset \forall v\forall wA'(w)$, in the following way:

$$ \frac{\frac{A'(t) \to A'(t)}{\forall vA'(v) \to A'(t)}}{\frac{\forall vA'(v) \to \forall wA'(w)}{\forall vA'(v) \to \forall v\forall wA'(w)}} \forall_l \forall_r $$

A useful feature of the standard translation is that we can easily recognize whether a formula in $\mathcal{SL}$ originates from a modal formula by examining the structure of its world quantifiers.

In translations of modal formulas, each subformula is always bound by the innermost world quantifier that it is in the scope of.

For example, consider the modal formula $\Box\Diamond P$ which translates to $\forall w\exists uP'(u)$. Here, the variable $u$ in the predicate $P'(u)$ is bound by the innermost world quantifier $\exists u$. That is, we will not get a formula from the translation in which different world-quantifiers bind the same subformula "cross-wise". The subformula $Q'(v) \wedge P'(w)$ in the formula $\forall w\forall v(Q'(v) \wedge P'(w))$, for example, is in the scope of both world quantifiers $\forall w$ and $\forall v$, even though the subformulas $Q'(v)$ and $P'(w)$ are only bound by one of them respectively, and the innermost world quantifier that the subformula $P'(w)$ is in the scope of does not bind it. In this case, we say that the world-quantifiers *cross-bind*. In contrast, the world quantifiers in the translation $(\forall v(Q'(v) \wedge \exists wP'(w))) \wedge T'(u)$ of the formula $(\Box(Q \wedge \Diamond P)) \wedge T$ do not cross-bind as the subformulas that are being bound are bound by the innermost world-quantifier that they are in the scope of. Thus, formulas in $\mathcal{SL}$ in which world-quantifiers cross-bind express relations between worlds which cannot be expressed in modal logic. These observations motivate the definition of the *one-world-variable fragment*.

**Definition 10.** Let $v$ be some world variable. Then the one-world-variable fragment $\mathcal{SL}^v$ contains the formulas in the two-sorted logic $\mathcal{SL}$ in which every subformula is only bound by the innermost world quantifier. The only free world variable that might appear in a subformula is $v$, in which case the subformula is not in the scope of any other world-quantifier.

**Lemma 2.** For every quantified modal S5-formula $\varphi$, its translation $ST_v(\varphi)$ belongs to $\mathcal{SL}^v$ that can be expressed with a single bound world variable. In contrast, every formula in $\mathcal{SL}^v$ is the translation $ST_v(\varphi)$ of some formula $\varphi$ in $\mathcal{QML}$.
*Proof.* The first implication of the lemma can be easily derived from the definition of the translation $ST_v$. Conversely, we can construct a “re-translation” of formulas in one-world-variable fragment $SL_v$ to quantified modal formulas:

$$ 
\begin{aligned}
Re_v : SL^v & \to QML \\
P(v, x_1, \dots, x_n) & \mapsto P(x_1, \dots, x_n) \\
\bot & \mapsto \bot \\
\varphi \wedge \psi & \mapsto Re_v(\varphi) \wedge Re_v(\psi) \\
\neg \varphi & \mapsto \neg Re_v(\varphi) \\
\forall x \varphi & \mapsto \forall x Re_v(\varphi) \\
\forall v \varphi & \mapsto \Box Re_v(\varphi)
\end{aligned}
$$

It is easily checked that for every formula $\varphi$ in $SL^v$, we have that $\varphi = ST_v(Re_v(\varphi))$ and thus it is the translation of the formula $Re_v(\varphi)$ in $QML$.

The fragment $SL^v$ captures exactly those formulas in the two-sorted logic that correspond to modal S5 formulas with a single bound world variable per scope. This fragment provides a syntactic criterion for deciding retranslatability, and separates formulas with true modal structure from those which are only expressible in the extended two-sorted language. Its role is central in distinguishing genuine modal interpolants from purely logical ones.

**Proposition 2.** A modal formula $\varphi$ is valid in (constant domain) S5 if and only if its translation $\varphi'$ is valid in the two-sorted first-order logic.

*Proof.* The modalities are replaced inside-out by first-order quantifiers, binding all world positions which are free, and thus not bound yet.

*Example 1.* Consider the formula $\Box(\forall x A(x) \supset \Diamond \exists y A(y))$. This formula can be translated first to $\Box(\forall x A(x) \supset \exists w \exists y A'(w, y))$, and then to $\forall v(\forall x A'(v, x) \supset \exists w \exists y A'(w, y))$.

# 5 Proof-Theoretic Properties of $SL$

The tools available in two-sorted logic are those familiar from classical first-order logic. In particular, it is possible to define a Gentzen-style sequent calculus for $SL$. The main adjustment lies in the treatment of quantifiers: when applying quantifier introduction rules, we must ensure that variables replace terms of the appropriate sort - either world or object. Aside from this consideration, the inference rules remain essentially unchanged. As a result, standard results such as the cut-elimination theorem, Maehara's lemma, and Craig's interpolation theorem all hold in $SL$.

**Theorem 3.** $SL$ admits cut-elimination.
*Proof (Sketch).* The structure of proof transformations mirrors the usual Gentzen system. The proof is similar to Gentzen's proof, with the difference that we consider a combined rank $r(\varphi)$ for two-sorted formulas to be the sum of the complexity from the object part and the world part of a formula $\varphi$.

We have the following consequence.

**Corollary 2.** *SL* admits the Maehara's lemma for cut-free proofs.

We briefly sketch the proof strategy for the extended mid-sequent theorem in the two-sorted sequent calculus for *SL*. This mirrors the Gentzen-style mid-sequent constructions, adapted for a two-sorted system.

**Theorem 4 (Extended mid-sequent theorem).** Let $\Gamma \vdash \Delta$ be a sequent in the two-sorted cut-free calculus *SL*, such that all world quantifiers in $\Gamma \vdash \Delta$ are prenex. Then there exists a mid-sequent $\Sigma \vdash \Pi$ such that above the mid-sequent there are only inferences involving world quantifiers and propositional rules, and below the mid-sequent are only inferences involving object quantifiers and structural rules.

*Proof (Sketch).* The proof proceeds by structural induction on the cut-free proof. We start with a cut-free proof of the given sequent. Identify object quantifier inferences ($\forall x, \exists x$) that are above propositional or world quantifier rules. Push these quantifier inferences down through the derivation by permuting them with:

- Propositional rules (e.g., $\wedge, \vee, \supset$) - which do not interfere with quantifier bindings;

- World/modal quantifiers - since *SL* uses sorted variables, these don't interfere.

Repeat until all object quantifier inferences are strictly below a chosen sequent (the mid-sequent), and the rest (world, propositional) are above. This reordering is sound because world and object quantifiers operate over disjoint classes of variables, so eigenvariable conditions remain preserved. At each step, structural rules (such as weakening and contraction) are permuted as needed. This allows us to stratify the derivation with a mid-sequent separating object quantifier reasoning from world quantifier reasoning.

The extended mid-sequent theorem yields several important consequences:

**Corollary 3.** For every valid prenex formula in S5 of the form $\exists x_1 \dots \exists x_n \varphi$, where $\varphi$ is quantifier-free and may contain modalities, there exists a Herbrand disjunction:

$$ \varphi(t_1^1, \dots, t_n^1) \lor \dots \lor \varphi(t_1^k, \dots, t_n^k) $$

which is equivalent (in *SL*) to the original formula.
**Proof.** By the extended mid-sequent theorem, any derivation of a valid prenex formula in S5 admits a mid-sequent in which all object quantifier inferences are pushed below the propositional modal inferences. The resulting mid-sequent consists of a disjunction of quantifier-free instances, each of which corresponds to a formula in $SL^V$ and represents a possible Herbrand expansion. The derivability of the disjunction follows by standard arguments from the cut-free calculus and modal interpretation of the two-sorted logic.

**Remark 1.** Unlike in classical logic, we do not require quantifier rules for both sorts to occur in the same fragment: the modal quantifiers may appear throughout the derivation. This is crucial for applications in modal logic, where the modal structure reflects the Kripke semantics and propositional S5 already lacks a standard analytic calculus.

The main novelty is that we only reorganize the proof with respect to object quantifier rules, leaving modal ones untouched.

**Corollary 4.** *The prenex fragment of quantified modal logic S5 admits Skolemization. That is, existential quantifiers may be replaced by Skolem functions without loss of validity in this fragment. The extended mid-sequent theorem ensures that Skolem terms do not need to depend on world variables.*

The Skolemization described above directly corresponds to the second epsilon theorem [12]. Skolemization fails in full quantified S5:

**Proposition 3.** *The implication $\Box A(c) \supset \exists x \Box A(x)$ is valid in constant domain S5. However, the converse $\exists x \Box A(x) \supset \Box \exists x A(x)$ fails.*

*Proof (Sketch).* This is a standard failure of modal quantifier shifts in constant domain semantics. While

$$ \Box A(c) \supset \exists x \Box A(x) $$

holds due to domain constancy,

$$ \exists x \Box A(x) \supset \Box \exists x A(x) $$

does not, because the witness for the existential quantifier in the accessible world may not be fixed across all worlds. A countermodel can be given with two worlds where the existential is satisfied in one, but the boxed existential fails globally.

Note that therefore Craig's interpolation theorem holds for all valid implications, however the interpolant is not always re-translatable in the language of quantified S5.

# 6 Interpolation

Interestingly, in our two-sorted logic $SL$ (with full cut-elimination and the mid-sequent theorem), we can still extract an interpolant $I$ - the system is expressive enough. However:
**Proposition 4.** Any interpolant obtained in $\mathcal{SL}$ for Kit Fine's counterexample is not equivalent to any formula in the syntax of quantified S5.

*Proof.* From the cut-free proof in $\mathcal{SL}$, Maehara's lemma yields an interpolant $I$. But this formula contains quantifier structures or term dependencies (from the two-sorted framework) that cannot be translated back into any formula of quantified S5. Thus, while $I$ exists in $\mathcal{SL}$, there is no $I'$ in the syntax of S5 such that $I = I'$.

## 6.1 Propositional Interpolation for S5

Propositional interpolation for S5 is known, but our new proof uses Maehara's lemma. Even in Fine's counterexample, interpolants exist but are not expressible in S5.

**Proposition 5.** *Propositional S5 interpolates.*

*Proof.* The propositional implication $A \supset B$ corresponds in the language of S5 to the monadic sequent $A' \to B'$. The Maehara interpolant is therefore a monadic expression. We consider an innermost $\forall$ on the right. We use a conjunctive normal form, a distribution and a confinement of the universal quantifiers to the negated and unnegated atoms where it actually binds the worlds (dual for $\exists$). By this procedure any of these world quantifiers binds all worlds in its scope, and the formula can be therefore understood as S5 formula. (Note that this procedure increases the size of interpolants.)

*Example 2.* Let $C, D, P$ and $Q$ be 0-place predicate symbols in constant domain S5 (so we are talking about formulas in propositional logic). We will try to find the interpolant of the following valid sequent consisting of non-prenex formulas:

$$ \diamond((P \lor P) \land C), \diamond((Q \lor Q) \land C) \rightarrow \diamond(P \lor D) \land \diamond(Q \lor D), \diamond P, \diamond Q $$

As can be easily checked, a suitable interpolant in constant domain S5 would be the formula $\diamond P \land \diamond Q$. Let us see what kind of interpolant we get from applying Maehara's lemma.

1. Translate to $\mathcal{SL}$:

$$ \forall v((P'(v) \lor P'(v)) \land C'(v)), \forall v((Q'(v) \lor Q'(v)) \land C'(v)) \rightarrow \\ \forall v(P'(v) \lor D'(v)) \land \forall v(Q'(v) \lor D'(v)), \forall vP'(v), \forall vQ'(v) $$

2. Use Maehara's Lemma to construct the interpolant from the proof of the translated formula: $\varphi_1 =$
$$ \frac{\frac{P'(u) \to P'(u) \qquad P'(u) \to P'(u)}{P'(u) \lor P'(u) \to P'(u)} \lor_l \frac{P'(u) \lor P'(u) \to P'(u), P'(u)}{P'(u) \lor P'(u) \to P'(u) \lor D'(u), P'(u)} \lor_r \frac{(P'(u) \lor P'(u)) \land C'(u) \to P'(u) \lor D'(u), P'(u)}{(P'(u) \lor P'(u)) \land C'(u) \to \exists v(P'(v) \lor D'(v)), P'(u)} \land_l \frac{(P'(u) \lor P'(u)) \land C'(u) \to \exists v(P'(v) \lor D'(v)), P'(u)}{(P'(u) \lor P'(u)) \land C'(u), (Q'(b) \lor Q'(b)) \land C'(b) \to \exists v(P'(v) \lor D'(v)), P'(u), Q'(b)} \lor_r \frac{w_r}{w_l}}{S_1: (P'(u) \lor P'(u)) \land C'(u), (Q'(b) \lor Q'(b)) \land C'(b) \to \exists v(P'(v) \lor D'(v)), P'(u), Q'(b)} \lor_w w_r} $$

and $\varphi_2 =$

$$ \frac{\frac{Q'(b) \to Q'(b) \qquad Q'(b) \to Q'(b)}{Q'(b) \lor Q'(b) \to Q'(b)} \lor_l \frac{Q'(b) \lor Q'(b) \to Q'(b), Q'(b)}{Q'(b) \lor Q'(b) \to Q'(b), Q'(b)} \lor_r \frac{Q'(b) \lor Q'(b) \to Q'(b) \lor D'(b), Q'(b)}{(Q'(b) \lor Q'(b)) \land C'(b) \to Q'(b) \lor D'(b), Q'(b)} \land_l \frac{(Q'(b) \lor Q'(b)) \land C'(b) \to \exists v(Q'(v) \lor D'(v)), Q'(b)}{(Q'(b) \lor Q'(b)) \land C'(b) \to \exists v(Q'(v) \lor D'(v)), Q'(b)} \lor_r \frac{w_l}{w_r}}{S_2: (P'(u) \lor P'(u)) \land C'(u), (Q'(b) \lor Q'(b)) \land C'(b) \to \exists v(Q'(v) \lor D'(v)), P'(u), Q'(b)} \lor_w w_r} $$

We then obtain

where

$$ F_1 = (P'(u) \lor P'(u)) \land C'(u), $$

and

$$ F_2 = \exists v((P'(v) \lor P'(v)) \land C'(v)). $$

By inductively reconstructing the interpolant using Maehara's lemma, we get the interpolant

$$ I' = \exists w \exists v P'(v) \land Q'(w). $$

By shifting quantifiers we obtain $\exists v P'(v) \land \exists w Q'(w)$, a retranslation of what corresponds to the formula $\diamond P \land \diamond Q$.

## 6.2 Interpolation for Weak Fragments

We now consider a fragment of quantified modal S5 in which the object quantifiers and/or the modal operators are weak. Recall that a quantifier occurrence is said to be *strong* if it occurs positively as $\forall x$ or negatively as $\exists x$, *weak* if it occurs negatively as $\forall x$ or positively as $\exists x$. This syntactic condition ensures that quantifiers occur only in positions where they may be expanded into finite
conjunctions or disjunctions during cut-free derivations, without violating the eigenvariable condition. As a result, the quantifiers can be eliminated and reintroduced purely propositionally. Modalities are analogously defined: □ is strong in positive and ◊ is strong in negative positions; otherwise, they are weak.

**Theorem 5.** Let A ⊃ B be a valid implication in S5, where both the antecedent and succedent contain arbitrary quantifiers but only weak modalities. Then there is a formula I in the common language of A and B such that A ⊃ I and I ⊃ B are valid in S5.

*Proof.* Let A' ⊃ B' be the translation of A ⊃ B to SL and I' its interpolant according to Craig's interpolation theorem. Note that all terms in worlds quantifier inferences can be restricted to one free-world variable a. Do not infer the world quantifiers, construct a first-order interpolant, and reintroduce the world quantifiers.

**Corollary 5.** If both quantifiers and modalities are weak, the interprolant is a propositional modal-free formula.

*Proof.* We neither infer the weak world quantifiers nor the weak object quantifiers. Instead, we construct a propositional interpolant and then we reintroduce the quantifiers to restore the full logical context. The result is a modal-free propositional interpolant.

## 6.3 Interpolation for the Prenex Fragment

Here we show that interpolation holds in the prenex fragment of S5 by leveraging the extended mid-sequent theorem and a variant of Maehara's lemma. The key idea is that the quantifier prefix can be treated uniformly, and the modal-propositional matrix admits interpolation. The quantifier prefix can then be reintroduced, yielding an interpolant that also belongs to the prenex fragment.

**Theorem 6.** Let A' ⊃ B' be a valid implication in S5, where both the antecedent and succedent are prenex formulas of the form QxA(x) and QyB(y), where A and B contain no object quantifiers and Qx and Qy are object quantifiers only. Then there is a formula I in the common language of QxA(x) and QyB(y) such that QxA(x) ⊃ I and I ⊃ QyB(y) are valid in S5.

*Proof.* By the extended mid-sequent theorem we have the Herbrand disjunction

$$A(\bar{t}_1) \dots A(\bar{t}_m) \rightarrow A(\bar{s}_1) \dots A(\bar{s}_n)$$

which has an interpolation I' which is the picture of a propositional modal interpolant I. Then, we infer the quantifiers accordingly.
# 7 Conclusion and Future Works

This work presents a syntactic proof-theoretic account of interpolation for first-order modal logic S5 via a two-sorted sequent calculus $SL$, emphasizing mid-sequent theorems and cut-elimination. Unlike in the propositional setting, interpolation in first-order modal logic cannot, in general, be treated purely semantically. As Harvey Friedman showed [10], no recursive bound exists on the size of interpolants in classical logic, making semantic existence results non-constructive. Our calculus offers an explicit framework for extracting interpolants (and bounding their size syntactically). All results of this paper are simple consequences of the analytic sequent calculus for the semantics of S5. In this respect, many further results can be obtained, for example a classification of Skolemizing fragments according to an investigation in which cases the world positions can be removed from Skolem functions.

Interpolants derived via Maehara's lemma in $SL$ may not always be retranslatable into the modal syntax. However, when quantifier scopes obey a one-variable discipline, such interpolants correspond to standard modal translations. Retranslation, when possible, often requires exponential unfolding, raising an open complexity question:

*Are interpolants in* $SL$ *significantly smaller than their modal counterparts?*

We leave a detailed comparison for future work. However, the process of retranslating such an interpolant into an equivalent S5 formula - when possible - typically requires a nontrivial transformation. This transformation corresponds to a form of “unwinding”, which resembles a decision procedure over the monadic fragment of first-order logic.

Given that monadic first-order logic is decidable but nontrivial in complexity (cf. the Bernays-Schönfinkel class), this suggests that:

- Interpolants in $SL$ may be computationally or structurally more efficient;

- Their S5-translations may be longer or less optimal;

- This asymmetry emphasizes again the expressive strength of the two-sorted framework.

**Aknowledgement.** We thank Charlotte Jergitsch, as this paper extends her Master's thesis [14]. We also acknowledge helpful discussions and suggestions from colleagues throughout the development of this work.

# References

1. Barkan, H.: On the interpretation of modal logic. Theoria 30(2), 146–153 (1964)

2. Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, vol. 3, chap. 1. Elsevier (2007)

3. Braüner, T., Ghilardi, S.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, vol. 3, chap. 9. Elsevier (2007)
4. Ciabattoni, A., Galatos, N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, Pittsburgh, PA, USA, 24–27 June 2008. pp. 229–240. IEEE Computer Society (2008). https://doi.org/10.1109/LICS.2008.39

5. Ciabattoni, A., Galatos, N., Terui, K.: Algebraic proof theory for substructural logics: cut-elimination and analyticity. Ann. Pure Appl. Logic **163**(3), 266–290 (2009)

6. Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic **22**(03), 269–285 (1957)

7. Fine, K.: Failures of the interpolation lemma in quantified modal logic. J. Symb. Logic **44**(2), 201–206 (1979)

8. Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic, Synthese Library, vol. 277. Springer, Cham (1998)

9. Flum, J., Ziegler, M.: Interpolation theorems for fragments of first-order modal logic. Math. Log. Q. **36**(1), 95–104 (1990)

10. Friedman, H.: The complexity of explicit definitions. Adv. Math. **20**(1), 18–29 (1976). https://doi.org/10.1016/0001-8708(76)90167-5. https://www.sciencedirect.com/science/article/pii/0001870876901675

11. Gabbay, D.M.: Semantical investigations in heyting's intuitionistic logic. In: Synthese Library. Springer, Cham (1981), chapter on interpolation failures

12. Hilbert, D., Bernays, P.: Grundlagen der mathematik. Springer, Cham (1934)

13. Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routledge (1996)

14. Jergitsch, C.: Interpolation by translation. Master’s thesis, TU Wien, Vienna, Austria (2023). http://hdl.handle.net/20.500.12708/176748

15. Maksimova, L.: Intuitionistic logic and implicit definability. Ann. Pure Appl. Logic **105**(1–3), 83–102 (2000)

16. Maksimova, L.L.: Craig’s theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras. Algebra Logic **16**(6), 427–455 (1977)

17. Maksimova, L.L.: Interpolation properties of superintuitionistic logics. Stud. Logica. **38**(4), 419–428 (1979)

18. Steinacker, P.: Modallogik. In: Nichtklassische Logik - eine Einführung, chap. 3. Akademie-Verlag, Berlin (1988)

19. Sturm, H., Wolter, F.: First-order expressivity for s5-models: modal vs. two-sorted languages. J. Philos. Logic **44**(2), 201–206 (2000)

20. Takeuti, G.: Proof theory. Studies in Logic and the Foundations of Mathematics, 2nd edn. North-Holland (1987). https://doi.org/10.1016/S0049-237X(08)70603-7. https://www.sciencedirect.com/science/article/pii/S0049237X08706037

21. Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE **103**(11), 2021–2035 (2015)
**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

<figure><img src="image_19.png" /></figure>
# Deciding Satisfiability for Overlaid Symbolic Heaps

Nicolas Peltier¹ Ⓒ, Quentin Petitjean²(✉) Ⓒ, and Mihaela Sighireanu² Ⓒ

¹ Univ. Grenoble Alpes, CNRS, LIG, 38000 Grenoble, France

² Univ. Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190 Gif-sur-Yvette, France
quentin.petitjean@ens-paris-saclay.fr

**Abstract.** Separation logic (SL) is a widely used formalism for verifying programs that manipulate dynamically allocated memory, relying on the separating conjunction ⋆ to combine disjoint heap structures. The standard approach in SL lacks the expressive power to handle overlaid data structures where multiple structures share some locations. We consider a logic that extends SL with a new separating conjunction operator ⊗, enabling the composition of heaps with shared locations that allocate distinct fields. Our fragment supports generic inductive definitions and introduces set variables to constrain the locations shared by overlapping structures. We prove that the satisfiability problem for this fragment is in NEXPTIME, by reducing it to the satisfiability problem in BAPA [11], a decidable logic combining Boolean algebra of sets and Presburger arithmetic.

**Keywords:** Separation logic · Satisfiability problem · Overlaid structures · BAPA

## 1 Introduction

Separation logic (SL) [9,21] is widely employed in program verification. It extends Hoare logic to enable reasoning about programs that manipulate dynamically allocated memory. In SL, formulæ are constructed using two types of atoms: the first, denoted $x \rightarrow (y_1, \dots, y_k)$, indicates that a memory block containing the tuple formed by the values of $y_1, \dots, y_k$ is allocated at (and only at) location $x$; the second, emp, represents the empty heap, i.e., a heap with no allocated locations. These atoms are combined into formulæ using logical connectives, including a distinctive operator known as the *separating conjunction* written ⋆. The formula $\varphi_1 \star \varphi_2$ asserts that $\varphi_1$ and $\varphi_2$ hold on disjoint portions of the heap. This connective enables *local reasoning*, which enhances the scalability by allowing program properties to be asserted and verified solely with reference to the heap regions it affects. Additionally, to support the specification of recursive data structures, SL incorporates predicate atoms defined by inductive rules with fixpoint semantics. For example, list segments from $x$ to $y$ may be defined by the

<footnote>This work has been partially funded by the French National Research Agency project ANR-21-CE48-0011.</footnote>
following rules<fnref n="1" />:

$$lseg(x, y) \Leftarrow emp \star x \approx y, \quad lseg(x, y) \Leftarrow x \to (z) \star lseg(z, y). \quad (1)$$

The satisfiability and entailment problems have been extensively studied for various fragments of SL, particularly the so-called symbolic heaps fragment, which can be defined as (disjunctions of) existentially quantified separating conjunctions of atoms. It has been established that satisfiability in this fragment is EXPTIME-complete [2], while entailment is undecidable. For the latter problem, decidability can be achieved by restricting the form of the inductive rules defining predicate symbols (see, e.g., [4, 8, 17]).

However, this standard fragment of SL has limited expressive power. The connective $\star$ only permits the combination of disjoint structures, which precludes reasoning about structures that share elements—a common scenario in practical applications. For instance, consider a collection of pairwise disjoint sublists alongside an additional list containing all elements from these sublists in some arbitrary order; here, the sublists share nodes with the encompassing list. Another example is a tree structure whose leaves are linked in a list in an arbitrary order. Modelling an operation such as tree expansion would require removing a node $\alpha$ from the list of leaves and adding new nodes both to the list and as successors of $\alpha$ in the tree. In this case, the order of leaves in the list is arbitrary, so encoding the structure with a single inductive predicate (e.g., defining a tree with leaves chained from left to right) would not capture the intended class of structures, as the described operation would not preserve this invariant. Notably, in this example, only some nodes (the leaves) are shared, while inner nodes remain distinct. Such data structures, where locations may be shared across multiple structures, are termed “overlaid”.

To address this limitation, various fragments of SL have been explored. Some offer sound decision procedures for program analysis [3, 6, 15, 16], while others eschew inductive definitions in favour of an indexed separation conjunction combined with flow equations [10, 18]. Notably, the logic NOLL [6] can describe nested linked lists with shared nodes, with satisfiability and entailment being NP-complete and co-NP-complete, respectively. To our knowledge, however, no fragment of SL fully addresses generic overlaid data structures while providing decidability results.

Building on prior work investigating decidable fragments of SL [2, 4, 7, 14, 17, 20], we propose the logic OSL, inspired by [6, 8], that supports overlaid data structures. Specifically, we model the heaps as partial finite functions from pairs $(\ell, f)$ (where $\ell$ is a location and $f$ is a field) to tuples of locations. One field is thus allowed to make one location point to a tuple of locations. The use of different fields allows associating several tuples of locations with the same location. As a result, a single field is sufficient to support standard data structures of SL. Heaps are combined using the weak separating conjunction operator $\otimes$ (introduced in [6]), which allows shared locations to allocate distinct record fields. OSL extends the simple inductive definitions of [6] to more

<footnote n="1">¹ We distinguish the equality in formula $\approx$ from the mathematical equality $=$. Moreover, in this paper, we adopt the convention that equations $x \approx y$ are satisfied only if the heap is empty. This entails no loss of generality in our context and simplifies the input language, as standard conjunction becomes dispensable.</footnote>
general inductive definitions of [8], with the restriction that each inductive predicate allocates only one field. However, the value referenced by a field is a tuple of locations, enabling straightforward descriptions of tree-shaped structures; the key constraint is that a predicate cannot allocate multiple distinct fields. Additionally, the fragment incorporates set variables within inductive predicates to collect subsets of allocated locations. We use these variables in set constraints to impose conditions on the overlap between inductive structures.

To summarize, the classical conjunction ∧ asserts that a heap satisfies two properties; the standard separating conjunction ★ asserts that a heap can be divided into two sub-heaps, each satisfying one side of the separating conjunction; and lastly, the overlaid separating conjunction ⊗ allows the two sub-heaps to overlap, provided that overlapping locations are allocated using distinct fields.

*Example 1.* The tree-and-list example can be encoded in OSL as the formula $\mathit{tree}(x, Y) \otimes \mathit{ls}(y, Y)$, where the predicate atoms are defined by the following rules:

$$ \mathit{tree}(x, Y) \Leftarrow x.t \to () \star Y \approx \{x\}, \qquad (2) $$

$$ \mathit{tree}(x, Y) \Leftarrow x.t \to (x_1, x_2) \star \mathit{tree}(x_1, Y_1) \star \mathit{tree}(x_2, Y_2) \star Y \approx Y_1 \sqcup Y_2, \qquad (3) $$

$$ \mathit{ls}(y, Y) \Leftarrow y.l \to () \star Y \approx \{y\}, \qquad (4) $$

$$ \mathit{ls}(y, Y) \Leftarrow y.l \to (y') \star \mathit{ls}(y', Y') \star Y \approx \{y\} \sqcup Y', \qquad (5) $$

where the rules employ two distinct fields, *t* and *l*, to encode trees and lists respectively<fnref n="2" />. The symbols *x*, *y*, *y'*, *x*₁, *x*₂ denote location variables, while *Y*, *Y'*, *Y*₁, *Y*₂ represent sets of locations. The symbol $\sqcup$ stands for set union.

In this paper, we investigate the satisfiability problem for OSL and we demonstrate that it is in NEXPTIME. Reasoning about OSL formulae requires combining standard spatial reasoning in SL (to handle predicate definitions, equalities, and constraints ensuring that a given field is allocated only once) with cardinality constraints arising from shared set variables. For instance, the formula $\mathit{ls}_{\text{even}}(x, Y) \otimes \mathit{ls}_{\text{odd}}(x, Y)$ is unsatisfiable if $\mathit{ls}_{\text{even}}$ and $\mathit{ls}_{\text{odd}}$ describe lists of even and odd lengths with set variables collecting all locations, respectively. The formula $\mathit{ls}_1(x, X) \otimes \mathit{ls}_2(x, X)$ is satisfiable if $\mathit{ls}_1$ and $\mathit{ls}_2$ both denote non-empty lists, provided these lists are chained using distinct fields, while $\mathit{ls}_1(x, X) \star \mathit{ls}_2(x, X)$ is always unsatisfiable (as the lists are non-empty each structure must allocate *x*). We thus reduce the satisfiability problem for OSL to a satisfiability problem in the logic BAPA [12], which combines the Boolean algebra of sets of uninterpreted elements with Presburger arithmetic to capture cardinality constraints on sets.

All proofs are given in the appendix of the full version of the paper<fnref n="3" />.

## 2 Separation Logic with Overlaid Inductive Definitions

We introduce OSL, the variant of SL we propose for the specification of overlaid data structures. After presenting its syntax and semantics, we illustrate its specification power and introduce some of its fragments that will be used in the following sections.

<footnote n="2">² Both the lists and trees end at the empty tuple ().</footnote>

<footnote n="3">³ The full version is available here: [hal-05143101](https://hal.inria.fr/1000-05143101).</footnote>
## 2.1 Syntax

In the definition below, the (possibly indexed) symbols $\varphi$, $L$, $A$, $t$, $B$ and $T$ denote formally, equational atoms, arithmetic atoms, arithmetic terms, set atoms and set terms, respectively (the symbol $\approx$ is overloaded). The symbols $\Phi$, $\Omega$, $\mathfrak{A}$, $t$, $\mathfrak{B}$ and $\mathfrak{T}$ denote the corresponding sets of objects of each sort.

**Definition 1 (OSL formulæ).** Let $\mathcal{F}$ be a finite set of field symbols. Let $\mathcal{V}$ be a countably infinite set of location variables; let $\mathcal{S}$ be a countably infinite set of set variables, and let $\mathcal{P}$ be a set of spatial predicate symbols, where each symbol $p \in \mathcal{P}$ is associated with a unique arity $\#(p)$ (with countably infinite sets of predicate symbols of each arity). The set of OSL formulæ (or simply formulæ) $\varphi$ is inductively defined as follows:

$$ \Phi \ni \varphi := \mathbf{emp} \mid x.f \rightarrow (y_1, \dots, y_d) \mid L \mid B \mid A \mid \varphi_1 \lor \varphi_2 \\ \mid \varphi_1 \star \varphi_2 \mid \varphi_1 \star\flat \varphi_2 \mid p(x_1, \dots, x_{\#(p)-1}, X) $$

with:

$$ \Omega \ni L := x \approx y \mid x \not\approx y \qquad t \ni t := K \mid t_1 \oplus t_2 \mid K \odot t \mid |T| $$

$$ \mathfrak{A} \ni A := t_1 \approx t_2 \mid t_1 \not\approx t_2 \mid t_1 < t_2 \mid t_1 \not\prec t_2 \mid K \text{ div } t \mid K \text{ ndiv } t $$

$$ \mathfrak{B} \ni B := T_1 \approx T_2 \mid T_1 \not\approx T_2 \mid T_1 \subseteq T_2 \mid T_1 \not\supseteq T_2 $$

$$ \mathfrak{T} \ni T := \{x\} \mid X \mid \emptyset \mid T_1 \sqcup T_2 \mid T_1 \sqcap T_2 $$

where $\varphi_1, \varphi_2 \in \Phi$ are formulæ, $p \in \mathcal{P}$, $d \in \mathbb{N}$, $K \in \mathbb{Z}$, $x, y, x_1, \dots, x_{\#(p)-1}, y_1, \dots, y_d \in \mathcal{V}$, $f \in \mathcal{F}$ and $X \in \mathcal{S}$.

The definition above adheres to the standard SL fragment known as (disjunctive) symbolic heap, while incorporating additional features to enable the specification of overlaid data structures. Note that negations are not supported; thus, negated versions of some operators are added. To allow for overlaid data structures, the points-to atom $x.f \rightarrow (y_1, \dots, y_d)$ identifies a portion of the memory block allocated at location $x$ by a field $f$ (for convenience, the arity of fields ($d$) is not fixed). Another OSL-specific feature is the inclusion of set variables (in $\mathcal{S}$), denoting finite sets of locations, and set constraints in formulae. We write set variables in capital letters to distinguish them from location variables in $\mathcal{V}$. Set terms are composed from set variables and basic term $\emptyset$ and $\{x\}$ using union and intersection of sets. The set constraints $\mathfrak{B}$ and the arithmetic constraints $\mathfrak{A}$ are a subset of those in the logic BAPA [12]. The integer terms $t$ include arithmetic operations (addition $\oplus$ and multiplication $\odot$) and set cardinality denoted by $|T|$. For simplicity, we do not consider arithmetic variables (this is not restrictive, as they can be encoded by terms $|X|$ where $X$ is a fresh set variable). The link between set variables and the heap is established using predicate atoms. Thus, a predicate atom $p(x_1, \dots, x_{\#(p)-1}, X)$ has exactly one set argument, in addition to other arguments denoting locations. Intuitively, the set argument is intended to denote a subset of the locations allocated in the data structure specified by the predicate; it is defined in the predicate's definition. For readability, we assume that the set argument always occurs at the last position in the argument list. The last feature of OSL is the composition of formulæ
using the “overlaid” separating conjunction operator $\oplus$, in addition to the classic separating conjunction $\star$. Intuitively, $\oplus$ composes formulæ specifying portions of memory defined by different fields inside the allocated memory regions.

To introduce predicate definitions and the OSL semantics, we use the following notations. The cardinality of a set $X$ is denoted by $\text{card}(X)$. The set $\{x \in \mathbb{Z} \mid i \le x \le j\}$ is denoted by $\llbracket i, j \rrbracket$. The domain of a function $f$ is written $\text{dom}(f)$. The powerset of a set $S$ is written $\mathcal{P}(S)$. The set of free (location and set) variables occurring in $\varphi$ is denoted by $fv(\varphi)$. A substitution $\sigma$ is a function from $\mathcal{V}$ to $\mathcal{V}$, and from $S$ to $\mathfrak{T}$. Its domain, $\text{dom}(\sigma)$, is the set of variables $x$ such that $\sigma(x) \neq x$, and its image is $\text{img}(\sigma) = \sigma(\text{dom}(\sigma))$. For any expression $e$ (a variable, tuple, term or formula), we denote by $e\sigma$ the expression obtained from $e$ by replacing each free occurrence of a variable $x$ with $\sigma(x)$. We denote by $\{x_i \mapsto t_i \mid 1 \le i \le n\}$ the substitution that maps each variable $x_i$ to $t_i$, where $x_i \in \mathcal{V} \cup S$ and $t_i$ is either a variable or a set term.

An inductive rule associated with the predicate $p \in \mathcal{P}$ has the following form in OSL (up to associativity and commutativity of $\star$):

$$p(x_1, \dots, x_n, X) \Leftarrow x_r.f \rightarrow (\tilde{z}) \star \star_{i=1}^{m} q_i(\vec{y}_i, Y_i) \star \varphi \star \left( X \approx E \sqcup \bigsqcup_{u \in U} Y_u \right), \quad (6)$$

where $r \in \llbracket 1, n \rrbracket$ and the following syntactic restrictions are satisfied:

- the set variables $Y_i$ are pairwise distinct set variables and distinct from $X$;

- the set term $E$ is either the constant $\emptyset$ or the term $\{x_r\}$;

- $U \subseteq \llbracket 1, m \rrbracket$ (the set $U$ may be $\emptyset$, in which case $\bigsqcup_{u \in U} Y_u$ is $\emptyset$);

- the formula $\varphi$ is a $\star$-conjunction of pure equational atoms $L \in \mathcal{L}$.

The variables $x_1, \dots, x_n, X$ are called parameters of $p$. We refer to the variables that appear in the right-hand side of the rule but are not among the predicate's parameters as the rule's auxiliary variables. These auxiliary variables include, in particular, the set variables $Y_i$. Formally, they are defined as $fv(x_r.f \rightarrow (\tilde{z}) \star \star_{i=1}^{m} q_i(\vec{y}_i, Y_i) \star \varphi \star (X \approx E \cup \bigsqcup_{u \in U} Y_u)) \setminus \{x_1, \dots, x_n, X\}$. Our form of predicate rule extends classical inductive definitions of SL—such as those in [8]—by incorporating set parameters and set constraints. In the following, we shall assume that $U = \llbracket 1, m \rrbracket$. This assumption simplifies the presentation, but does not affect the expressive power of the predicate definitions.

**Remark 1.** The conditions provided are less restrictive than those imposed in [8] to ensure the decidability of the entailment problem. No constraint is imposed on the spatial part of the formula, except that exactly one location $x_r$ must be allocated in every rule<fnref n="4" />. However, the use of set constraints and arithmetic terms inside the rules is strictly limited: the only allowed constraint (besides equational atoms) is the equation $X \approx E \sqcup \bigsqcup_{u \in U} Y_u$, which relates the value of the set parameter $X$ to the sets computed by recursive calls. It is essential that $E$ contains only locations allocated by the rule, as this guarantees that the same location is added at most once to the computed set (this

<footnote n="4">⁴ This condition is imposed for technical convenience only and does not limit the expressive power of predicate definitions.</footnote>
ensures that *E* contains only allocated locations and facilitates the computation of the cardinality of *X* in Sect. 3.2). Note also that the rules do not contain the connective ⋆: as we will restrict the set of rules defining a predicate to use only one field (see Sect. 2.3), using this connective inside of a rule is pointless.

A set of inductive definitions (SID) $\mathcal{R}$ contains finitely many rules associated with predicate symbols in $\mathcal{P}$. We write $p(y_1, \dots, y_n, Y) \Leftarrow \mathcal{R} \ \psi$ if the SID $\mathcal{R}$ contains a rule $p(x_1, \dots, x_n, X) \Leftarrow \varphi$, with $\psi = \varphi\{X \mapsto Y, x_i \mapsto y_i \mid i \in [1, n]\}$.

**Example 2.** The following OSL formula specifies a heap where a (non-empty) binary tree treel(r, h, N) and a list segment ls(h, l, S) are overlaid such that the list starts in the left-most leaf of the tree h and contains some of this leaf’s ancestors ($S \subseteq N$); the list ends into an empty memory block (l):

$$ (\mathit{treel}(r, h, N) \ominus \mathit{ls}(h, l, S)) \star S \subseteq N \star l.\mathit{next} \to () \quad (7) $$

The two predicates treel and ls are defined by the following rules:

$$ \mathit{treel}(x_r, x_l, X) \Leftarrow x_r.\mathit{sons} \to () \star x_l \approx x_r \star X \approx \{x_r\}, \quad (8) $$

$$ \mathit{treel}(x_r, x_l, X) \Leftarrow x_r.\mathit{sons} \to (y_l, y_r) \star x_l \not\approx x_r \star \mathit{treel}(y_l, x_l, Y_l) \star \mathit{tree}(y_r, Y_r) \quad (9) $$

$$ \star X \approx \{x_r\} \sqcup Y_l \sqcup Y_r, $$

$$ \mathit{tree}(x_r, X) \Leftarrow x_r.\mathit{sons} \to () \star X \approx \emptyset, \quad (10) $$

$$ \mathit{tree}(x_r, X) \Leftarrow x_r.\mathit{sons} \to (y_l, y_r) \star \mathit{tree}(y_l, Y_l) \star \mathit{tree}(y_r, Y_r) \quad (11) $$

$$ \star X \approx Y_l \sqcup Y_r, $$

$$ \mathit{ls}(x, y, X) \Leftarrow x.\mathit{next} \to (y) \star x \not\approx y \star X \approx \{x\}, \quad (12) $$

$$ \mathit{ls}(x, y, X) \Leftarrow x.\mathit{next} \to (z) \star x \not\approx y \star \mathit{ls}(z, y, Y) \star X \approx \{x\} \sqcup Y. \quad (13) $$

The auxiliary variables in rule 9 are $y_l$, $y_r$, $Y_l$ and $Y_r$.

## 2.2 Semantics

**Definition 2 (OSL structure).** Let $\mathcal{L}$ be a countably infinite set of so-called locations. An OSL structure is a tuple $(s, \mathfrak{h}, \Sigma)$ where $\mathfrak{s}$ is a store, i.e., a partial function from $\mathcal{V}$ to $\mathcal{L}$, $\mathfrak{h}$ is a heap, i.e., a partial finite function mapping pairs $(\ell, f)$ (where $\ell \in \mathcal{L}$ and $f \in \mathcal{F}$) to tuples of locations in $\mathcal{L}^*$ and $\Sigma$ is a set interpretation, i.e., a partial function mapping set variables in $\mathcal{S}$ to finite subsets of $\mathcal{L}$.

Thus $\mathrm{dom}(\mathfrak{h}) \subseteq \mathcal{L} \times \mathcal{F}$ for all heaps $\mathfrak{h}$. We denote by $\mathrm{dom}_f(\mathfrak{h})$ the set $\{\ell \mid (\ell, f) \in \mathrm{dom}(\mathfrak{h})\}$ and by $\mathrm{allocated}(\mathfrak{h})$ the set $\{\ell \mid \exists f \in \mathcal{F}. (\ell, f) \in \mathrm{dom}(\mathfrak{h})\}$. For conciseness, we omit in the following the semantics of arithmetic terms $t$ and arithmetic constraints $A$; their semantics is the expected one.

**Definition 3 (Semantics of set terms).** Let $T$ be a set term, $\mathfrak{s}$ be a store, and $\Sigma$ be a set interpretation. The interpretation of set term denoted by $[T]_{(s,\Sigma)}$ is a set of locations in $\mathcal{L}$ and it is inductively defined by the following rules:
$$- [\emptyset]_{(s, \Sigma)} = \emptyset;$$

$$- [\{x\}]_{(s, \Sigma)} = \{s(x)\};$$

$$- [X]_{(s, \Sigma)} = \Sigma(X);$$

$$- [T_1 \sqcup T_2]_{(s, \Sigma)} = [T_1]_{(s, \Sigma)} \cup [T_2]_{(s, \Sigma)};$$

$$- [T_1 \sqcap T_2]_{(s, \Sigma)} = [T_1]_{(s, \Sigma)} \cap [T_2]_{(s, \Sigma)}.$$

**Definition 4 (OSL semantics).** Given a formula $\varphi$, an SIDR and a structure $(s, h, \Sigma)$ with $fv(\varphi) \subseteq \text{dom}(s) \cup \text{dom}(\Sigma)$, the satisfaction relation $\models_R$ is inductively defined as the least relation such that $(s, h, \Sigma) \models_R \varphi$ iff one of the following conditions holds:

$$- \varphi = \text{emp} \text{ and } h = \emptyset;$$

$$- \varphi = (x.f \to (y_1, \dots, y_d)) \text{ and } h = [(s(x), f) \mapsto (s(y_1), \dots, s(y_d))];$$

$$- \varphi = (x \approx y), s(x) = s(y) \text{ and } h = \emptyset; \text{ or } \varphi = (x \not\approx y), s(x) \neq s(y) \text{ and } h = \emptyset;$$

$$- \varphi = \varphi_1 \lor \varphi_2 \text{ and } (s, h, \Sigma) \models_R \varphi_i, \text{ for some } i \in \{1, 2\};$$

$$- \varphi = \varphi_1 \star \varphi_2 \text{ and there exist heaps } h_1, h_2 \text{ such that } h = h_1 \cup h_2, \text{ allocated}(h_1) \cap \text{allocated}(h_2) = \emptyset \text{ and } (s, h_i, \Sigma) \models_R \varphi_i, \text{ for all } i \in \{1, 2\};$$

$$- \varphi = \varphi_1 \oplus \varphi_2 \text{ and there exist heaps } h_1, h_2 \text{ such that } h = h_1 \cup h_2, \text{dom}(h_1) \cap \text{dom}(h_2) = \emptyset \text{ and } (s, h_i, \Sigma) \models_R \varphi_i, \text{ for all } i \in \{1, 2\};$$

$$- \varphi = p(x_1, \dots, x_{\#(p)-1}, X), p \in \mathcal{P} \text{ and } (s', h, \Sigma') \models_R \psi, \text{ for some } s' \text{ matching } s \text{ on } x_1, \dots, x_{\#(p)-1}, \text{ some } \Sigma' \text{ matching } \Sigma \text{ on } X \text{ and for some } \psi \text{ such that } \varphi \Leftarrow_R \psi;$$

$$- \varphi = (T_1 \approx T_2), [T_1]_{(s, \Sigma)} = [T_2]_{(s, \Sigma)} \text{ and } h = \emptyset; \text{ the definition is similar for } \not\approx, \sqsubseteq, \not\sqsubseteq.$$

We write $\varphi \models_R \psi$ if for every structure $(s, h, \Sigma)$ we have $(s, h, \Sigma) \models_R \varphi \implies (s, h, \Sigma) \models_R \psi$. If both $\varphi \models_R \psi$ and $\psi \models_R \varphi$ hold, then we write $\varphi \equiv_R \psi$.

We emphasize that the atoms $x \approx y$ or $x \not\approx y$ only hold for empty heaps (this convention simplifies notations as it avoids the use of standard conjunction). The same convention applies to arithmetic and set constraints. Formulæ are taken modulo the usual properties of SL connectives: associativity and commutativity of $\star, \oplus$ and $\vee$, neutrality of $\text{emp}$ for $\star$ and $\oplus$, and commutativity of $\approx, \not\approx$. Intuitively, the interpretation of $\varphi_1 \star \varphi_2$ is stronger than that of $\varphi_1 \oplus \varphi_2$, as the latter allows for the allocation of the block at the same (starting) location in both $\varphi_1$ and $\varphi_2$, provided the considered offsets (represented by fields) are different. For instance, $x.f \to (y) \oplus x.g \to (y)$ is satisfiable, but not $x.f \to (y) \star x.g \to (y)$ or $x.f \to (y) \oplus x.f \to (y)$. Note that $h_1 \cup h_2$ is well defined if $\text{dom}(h_1) \cap \text{dom}(h_2) = \emptyset$ and that $\text{allocated}(h_1) \cap \text{allocated}(h_2) = \emptyset \implies \text{dom}(h_1) \cap \text{dom}(h_2) = \emptyset$. Thus $\varphi_1 \oplus \varphi_2$ is a logical consequence of $\varphi_1 \star \varphi_2$.

**Definition 5 (OSL model).** An $\mathcal{R}$-model of a formula $\varphi$ is a structure $(s, h, \Sigma)$ such that $(s, h, \Sigma) \models_R \varphi$. A formula $\psi$ admitting an $\mathcal{R}$-model is $\mathcal{R}$-satisfiable (or simply satisfiable if $\mathcal{R}$ is clear from the context).

## 2.3 1-Predicates

In the remainder of the paper, we assume that each predicate allocates a single field, in the sense that for every predicate $p \in \mathcal{P}$, there exists a unique field $f \in \mathcal{F}$ such that every points-to atom appearing in any unfolding of any atom $p(\vec{x}, X)$ is of the form $y.f \to (\vec{z})$, where $\vec{z}$ is a tuple of arbitrary length. More formally:
**Definition 6 (F-formulæ).** Let $F \subseteq \mathcal{F}$. The set of F-formulæ and F-predicates are defined co-inductively as the biggest sets satisfying the following conditions:

- if $x.f \to (\vec{v})$ is an F-formula then $f \in F$;

- if $\varphi_1 \bullet \varphi_2$ is an F-formula (for some binary connective $\bullet$) then $\varphi_1, \varphi_2$ are F-formulæ;

- if $p(\vec{x}, X)$ is an F-formula then $p$ is an F-predicate;

- if $p$ is an F-predicate and $p(\vec{x}, X) \Leftarrow \varphi \in \mathcal{R}$ then $\varphi$ is an F-formula.

A 1-predicate is a {$f$}-predicate, for some $f \in \mathcal{F}$.

In particular, pure formulæ are always F-formulæ for all $F$. If $\varphi$ is an {$f$}-formulæ, then it is clear that allocated($\mathfrak{b}$) $\subseteq$ dom$_f$($\mathfrak{b}$) holds for all models ($s, \mathfrak{b}, \Sigma$) of $\varphi$. Consequently, $\varphi_1 \star \varphi_2$ and $\varphi_1 \ominus \varphi_2$ are equivalent if $\varphi_1$ and $\varphi_2$ are both {$f$}-formulæ (with the same field $f$). Notice also that, due to the form of the rule in Eq. 6, we also have $\Sigma(X) \subseteq \text{dom}_f(\mathfrak{b})$.

## 2.4 Normal Form

The decision procedure proposed in Sect. 3 applies to a pair $(\varphi, \mathcal{R})$ in which both components are in normal form. This form can be obtained from general OSL formulæ and SID through a syntactic translation, which may cause an exponential increase in their respective sizes. We define this normal form below by gradually introducing its components.

*Symbolic Heap Formula.* As in classical SL, a *symbolic heap formula* [1] is a (separating) conjunction of atoms. This fragment is especially interesting for program analysis. A symbolic heap formula does not contain the $\vee$ connective. By distributivity of $\star$ and $\ominus$ over $\vee$, any OSL formula $\varphi$ can be transformed into an equivalent formula, denoted $dnf(\varphi)$, which is a disjunction of symbolic heap formulæ. Then, the satisfiability of $dnf(\varphi)$ can be tested by checking whether at least one of its disjuncts is satisfiable.

*Injective Store Models.* For proof's readability, we focus on models ($s, \mathfrak{b}, \Sigma$) where $s$ is injective on location variables. This is enforced by adding a disequation $x \neq y$ for every pair of distinct location variables $x, y$.

**Definition 7 (Normal form).** A pair $(\varphi, \mathcal{R})$ where $V$ is the set of location variables in $\varphi$ is in normal form if:

1. $\varphi$ is a symbolic heap and contains a disequation $x \neq y$ for every pair of distinct variables in $V$.

2. If $p(\vec{x}, X) \Leftarrow \psi$ is a rule in $\mathcal{R}$, $y, z \in V$, $y$ is an auxiliary variable in $\psi$ (i.e., a variable occurring in $\psi$ but not in $\vec{x}$) and $z$ is a variable distinct from $y$ occurring in $\vec{x}$ or $\psi$, then $\psi$ contains the atom $y \neq z$.

3. Each predicate $p$ ofarity $n+1$ is associated with a subset $I_p \subseteq \llbracket 1, n \rrbracket$ (called the main parameters of $p$), which satisfies the following properties:

- For every atom $p(x_1, \dots, x_n, X)$ occurring in $\varphi$ and every location variable $y$ in $V$, there exists $i \in I_p$ such that $x_i = y$;
- For every rule $p(x_1, \dots, x_n, X) \Leftarrow \psi$ and every atom $q(y_1, \dots, y_m, Y)$ in $\psi$, if $i \in I_p$, then there exists $j \in I_q$ such that $y_j = x_i$.

These conditions are designed to ensure that all location variables in $\varphi$ are passed as parameters to every predicate invoked during the evaluation of $\varphi$.

Condition 1 is not restrictive. Indeed, it is possible to enumerate all the equality relations on $V$ and test satisfiability of $\varphi$ for each of these relations, by replacing in $\varphi$ all the variables in the same equivalence class by the same representative and by adding disequations between distinct representatives. Condition 2 is easy to enforce: a rule of the form $p(\vec{x}, X) \Leftarrow \psi$ that includes an auxiliary variable $y$ and another (arbitrary) variable $z$ can be replaced by two rules: $p(\vec{x}, X) \Leftarrow \psi\{y \mapsto z\}$ and $p(\vec{x}, X) \Leftarrow \psi \star y \neq z$, thus distinguishing the cases where $y$ is equal to or different from $z$. Condition 3 is enforced by adding $|V|$ parameters to each predicate atom, corresponding to the variables in the set $V$. These additional parameters are simply propagated unchanged through recursive calls in predicate's rules.

**Remark 2.** As stated for all the components of the normal form, a general OSL formula and a SID can always be translated in normal form at the cost of a potential exponential increase in their respective sizes.

### 3 Satisfiability Problem

The satisfiability problem for OSL is defined as: "Given a formula $\varphi \in \Phi$ and a SID $\mathcal{R}$, does a structure $(s, \mathcal{h}, \Sigma)$ exist such that $(s, \mathcal{h}, \Sigma) \models_{\mathcal{R}} \varphi?"$ Our main contribution is stated by the following theorem, which identifies a sufficient condition to decide this problem.

**Theorem 1.** *The satisfiability problem for OSL is decidable in exponential space if the predicates defined by the SID are 1-predicates.*

The result is obtained in two main steps summarised in the remainder of this section. We assume that the pair $(\varphi, \mathcal{R})$ is in normal form. As shown in Sect. 2.4, this does not affect the expressive power of OSL.

The first step of the proof, presented in Sect. 3.1, introduces *decorations* of OSL for-mulæ. A decoration of a formula $\varphi$ partitions the models of $\varphi$ in such a way that each partition is characterized by (i) some aliasing and non-aliasing relations between the location variables, (ii) an assignment of location variables to the set variables, and (iii) an assignment of location variables to the allocated heap. Decorations are used to decorate predicate atoms and their defining rules in $\mathcal{R}$.

This results in a decorated SID $\mathcal{R}_{dec}$, in which only *consistent* rules are retained, namely, those where the partition induced by the decoration of the defining formula (i.e., the rule's right-hand side) is identical to the partition associated with the pred-icate being defined (i.e., the rule's left-hand side). This condition may be checked syntactically. Therefore, the initial question is split into $N$ questions for the pairs $(\varphi_d, \mathcal{R}_d)$ obtained by decorating $(\varphi, \mathcal{R})$, where $N$ is exponential in the size of the ini-tial pair. Intuitively, this exponential blow-up is due to enumerating all decorations, which involves enumerating equivalence relations between free location variables,
etc. The soundness and completeness of this step are stated by Theorem 2. Thus, if a formula $\varphi$ has a model $m$, then there exists a decoration $d$ such that the corresponding decorated formula $\varphi_d$ also has $m$ as a model. Conversely, if $\varphi_d$ has $m$ as a model, then $m$ is also a model of $\varphi$.

This first step serves two purposes: (i) it ensures that all constraints induced by unfolding a predicate atom can be identified solely by inspecting predicate's decoration; and (ii) it enables the description of the cardinality of set variables as a context-free grammar (which in turn can be transformed into a Presburger formula). To illustrate the second point, consider the rules $p(x, y, X) \Leftarrow x.f \rightarrow () \star X \approx \emptyset$ and $p(x, y, X) \Leftarrow x.f \rightarrow () \star x \neq y \star X \approx \{x\}$. If $(s, b, \Sigma) \models p(x, y, X)$, then $\text{card}(\Sigma(X)) = 0$ when $s(x) = s(y)$ (i.e., $x$ and $y$ alias), and $\text{card}(\Sigma(X)) \in \{0, 1\}$ otherwise. In contrast, if $(s, b, \Sigma) \models p_d(x, y, X)$ with $d$ a decoration, then the set of possible cardinalities of $\Sigma(X)$ depends only on the aliasing and non-aliasing relations in $d$: if $d$ imposes a non-aliasing of $x$ and $y$, then only the second rule can be unfolded and thus $\text{card}(\Sigma(X)) = 1$; if $d$ does not impose any condition on $x$ and $y$, then the first rule must be unfolded and $\text{card}(\Sigma(X)) = 0$; finally a decoration cannot impose an aliasing of $x$ and $y$ as there is no rule that requires such a condition. The second decoration admits models where $s(x) = s(y)$, but the cardinality of $X$ does not depend on $s$.

The second step, presented in Sects. 3.2 and 3.3, translates a decorated pair $(\varphi_d, \mathcal{R}_d)$ into an equi-satisfiable formula in the logic BAPA [11]. The translation preserves all the set constraints of $\varphi_d$ and it adds to them (a) Presburger formulæ that characterize the possible cardinalities of all set variables in $\varphi_d$; and (b) some set constraints encoding decorations, i.e., aliasing, non-aliasing, or membership constraints. Theorem 3 states that this translation is correct, i.e., it preserves satisfiability.

## 3.1 Decorations

**Definition 8 (Decorated predicate symbol).** Let $p \in \mathcal{P}$ be a predicate symbol of arity $n+1$. A decoration of $p$ is a symbol $p_{1, \mathcal{J}, \sim, \mathcal{F}}$ such that $I, J$ are subsets of $\llbracket 1, n \rrbracket$ with $I \subseteq J$, $\sim$ is an equivalence relation over (i.e., partition of) $\llbracket 1, n \rrbracket$ and $\mathcal{F}$ is a symmetric binary relation on $\llbracket 1, n \rrbracket$. The set of all decorations for symbols in $\mathcal{P}$ is denoted by $\mathcal{P}_{\text{dec}}$.

Intuitively, the decoration of a predicate symbol fixes certain aspects of the model of an atom $p(x_1, \dots, x_n, X)$. For instance, $p_{1, \mathcal{J}, \sim, \mathcal{F}}$ specifies that $I$ is the set of indices $i$ (i.e., parameter positions) such that $x_i$ occurs in $X$, and that $J$ is the set of indices $j$ such that $x_j$ is allocated. The relations $\sim$ and $\mathcal{F}$ encode aliasing and non-aliasing constraints, respectively: if $i \sim j$, then the store must map $x_i$ and $x_j$ to the same location; if $i \neq j$, then the locations of $x_i$ and $x_j$ must differ. Note that $i \neq j$ is not the negation of $i \sim j$, as both relations may be false in cases where no constraint is imposed on $x_i$ and $x_j$. If $i(\mathcal{F} \cap \sim) \neq \emptyset$, i.e., both $i \neq j$ and $i \sim j$ hold in a decoration, then the constraints resulting from the decoration are inconsistent; such decorations will be detected and eliminated in a later step (see Definition 14).

**Definition 9 (Decorated formula).** A formula $\psi$ is a decoration of a formula $\varphi$ if it is obtained from $\varphi$ by replacing every occurrence of a predicate symbol by a decoration of this symbol. A formula $\psi$ is a decoration if there exists a formula $\varphi$ such that $\psi$ is a decoration of $\varphi$.
Note that a predicate *p* symbol may appear in a formula with different decorations.

**Definition 10 (Aliasing of a decorated formula).** Let $\psi$ be a decoration of a symbolic heap formula with location variables $V$. The aliasing of $\psi$, denoted by $\equiv_\psi$, is the least reflexive, symmetric and transitive relation in $V^2$ such that $x \equiv_\psi y$ if one of the following conditions holds:

(a) $\psi$ contains an atom $x' \approx y'$ with $x \equiv_\psi x'$ and $y \equiv_\psi y'$;

(b) $\psi$ contains an atom $p_{I,J,\sim,\ne}(x_1, \dots, x_n, X)$ with $x_i \equiv_\psi x$, $x_j \equiv_\psi y$ and $i \sim j$.

Intuitively, $\equiv_\psi$ is the aliasing relation between the location variables of $\psi$ induced by the equality atoms and the decorations of predicate symbols.

**Definition 11 (Allocated variables).** Let $\psi$ be a decoration of a symbolic heap formula with location variables $V$. The set of variables allocated by $\psi$, denoted by $alloc(\psi)$, is a subset of $V$ inductively defined as the set of location variables $y$ such that one of the following conditions holds:

(a) $\psi$ contains an atom of the form $y.f \to (\tilde{z})$;

(b) $\psi$ contains an atom $p_{I,J,\sim,\ne}(x_1, \dots, x_n, X)$ such that $y = x_j$ with $j \in J$;

(c) $y \equiv_\psi y'$ with $y' \in alloc(\psi)$.

Intuitively, $alloc(\psi)$ denotes the set of variables in $V$ that must be allocated in every model of $\psi$, given the decoration of predicates in $\psi$ and the aliasing constraints.

**Definition 12 (Distinguishing of a decorated formula).** Let $\psi$ be a decoration of a symbolic heap formula with location variables $V$. The distinguishing of $\psi$, denoted $\ne_\psi$, is the least symmetric relation in $V^2$ such that $x \ne_\psi y$ if one of the following conditions holds:

(a) $\psi$ contains the atom $x \neq y$;

(b) $\psi$ contains the atom $p_{I,J,\sim,\ne}(x_1, \dots, x_n, X)$ with $x_i = x$, $x_j = y$ and $i \neq j$;

(c) $\psi$ contains $\psi_1 \star \psi_2$, $x \in alloc(\psi_1)$ and $y \in alloc(\psi_2)$;

(d) $x \equiv_\psi x'$, $y \equiv_\psi y'$ and $x' \neq_\psi y'$.

Intuitively, $\ne_\psi$ is the disequality relation between the location variables of $\psi$ induced by the disequality atoms, the decorations of predicate symbols and the separating conjunctions. The notion $\ne_\psi$ is only used in (and thus defined for) decorated formulæ that appear in a right hand side of a predicate rule. Note that if $\psi$ is in normal form, then $x \neq_\psi y$ holds for all distinct variables $x$ and $y$ occurring in $\psi$. However, this property does not necessarily hold for formulæ obtained through unfolding, as parameter instatiation may introduce aliasing.

**Definition 13 (Decorated set variable).** Let $\psi$ be a decoration of a symbolic heap formula with location variables $V$ and let $Y$ be a set variable. The set of location variables attached to $Y$ by $\psi$, denoted by $[Y]_\psi$, is inductively defined as the set of location variables $y \in V$ such that one of the following conditions holds:

(a) $\psi$ contains a set constraint $Y \approx E \sqcup \sqcup_{u \in U} Z_u$ (see Eq. 6) with $y \in E$ or $y \in [Z_u]_\psi$ for some $u \in U$;
(b) $\psi$ contains an atom $p_{I,J,\sim,\ne}(x_1, \dots, x_n, X)$ such that $X = Y$ and $y = x_i$ for some $i \in I$;

(c) $y \equiv_{\psi} y'$ with $y' \in [Y]_{\psi}$.

Intuitively, $[Y]_{\psi}$ is the subset of $V$, the location variables of $\psi$, that must be contained within the set variable $Y$ given the decoration of predicates in $\psi$ and the aliasing and set constraints.

**Definition 14 (Consistent decoration).** The decoration $\psi$ is consistent if the following condition holds: if $x \not\equiv_{\psi} y$ then $x \not\equiv_{\psi} y$.

**Definition 15 (Decorated rule).** Let $p$ be a predicate symbol, $p_{I,J,\sim,\ne}$ one of its decorations, and $p(x_1, \dots, x_n, X) \Leftarrow \varphi$ a rule defining $p$ in $\mathbb{R}$. A decorated rule for $p_{I,J,\sim,\ne}$ is a rule $p_{I,J,\sim,\ne}(x_1, \dots, x_n, X) \Leftarrow \psi$ satisfying all the conditions below:

- $\psi$ is a consistent decoration of $\varphi$;

- $i \sim j$ iff $x_i \equiv_{\psi} x_j$ for all $i, j \in [1, n]$; and $i \neq j$ iff $x_i \not\equiv_{\psi} x_j$ for all $i, j \in [1, n]$;

- $I = \{i \in [1, n] \mid x_i \in [X]_{\psi}\}$; and $J = \{j \in [1, n] \mid x_j \in \text{alloc}(\psi)\}$.

The set of decorated rules obtained from $\mathbb{R}$ and the decorated predicate symbols is called a decorated SID and it is denoted by $\mathbb{R}_{\text{dec}}$. The decoration of a pair $(\varphi, \mathbb{R})$ is a pair $(\psi, \mathbb{R}_{\text{dec}})$, where $\psi$ is a decoration of $\varphi$ and $\mathbb{R}_{\text{dec}}$ is the set of decorated rules obtained from $\mathbb{R}$.

**Example 3.** Consider the following predicate $p$ defined by the following rules in $\mathbb{R}$:

$$p(x, y, z, X) \Leftarrow x.f \rightarrow (y) \star x \neq y \star X \approx \emptyset, \quad p(x, y, z, X) \Leftarrow y.f \rightarrow (x) \star X \approx \{y\},$$

$$p(x, y, z, X) \Leftarrow z.f \rightarrow () \star X \approx \emptyset.$$

Let $\varphi = p(x, y, z, X) \star y \neq z \star z.f \rightarrow (x, y)$. The formula $\psi = p_{I,J,\sim,\ne}(x, y, z, X) \star y \neq z \star z.f \rightarrow (x, y)$ is a decoration of $\varphi$ with $y \not\equiv_{\psi} z$. If $\sim$ is the identity, then $\equiv_{\psi}$ is the identity. Moreover:

- If $I = \emptyset, J = \{1\}$ and $1 \neq 2$ then $x \not\equiv_{\psi} y$, $\text{alloc}(\psi) = \{x, z\}$ and $[X]_{\psi} = \emptyset$. The only rule associated with $p_{I,J,\sim,\ne}$ is: $p_{I,J,\sim,\ne}(x, y, z, X) \Leftarrow x.f \rightarrow (y) \star x \neq y \star X \approx \emptyset$.

- If $I = \{2\}, J = \{2\}$ and $\neq$ is empty then $\text{alloc}(\psi) = \{y, z\}$ and $[X]_{\psi} = \{y\}$. The only rule associated with $p_{I,J,\sim,\ne}$ is $p_{I,J,\sim,\ne}(x, y, z, X) \Leftarrow y.f \rightarrow (x) \star X \approx \{y\}$.

- If $I = \emptyset, J = \{3\}$ then the decoration is inconsistent because we obtain $z \not\equiv_{\psi} z$. Indeed, the only rule associated with $p_{I,J,\sim,\ne}$ is: $p_{I,J,\sim,\ne}(x, y, z, X) \Leftarrow z \rightarrow () \star X \approx \emptyset$; this rule allocates $z$ yielding a contradiction with the fact that $z$ is already allocated by $z.f \rightarrow (x, y)$ in $\psi$.

- If $I = J = \emptyset$ then $p_{I,J,\sim,\ne}$ has no rule, hence $p_{I,J,\sim,\ne}(x, y, z, X)$ (hence also $\psi$) is (trivially) unsatisfiable.

**Theorem 2.** Let $(\varphi, \mathbb{R})$ be a pair in normal form. For each structure $(s, b, \Sigma)$, we have $(s, b, \Sigma) \models_{\mathbb{R}} \varphi$ if and only if there exists a decoration $(\psi, \mathbb{R}_{\text{dec}})$ of $(\varphi, \mathbb{R})$ such that $(s, b, \Sigma) \models_{\mathbb{R}_{\text{dec}}} \psi$.
## 3.2 Cardinality Constraints

We now begin the second step of the proof, which translates a decorated pair $(\varphi_d, \mathcal{R}_d)$ in normal form into a Presburger formula. We first consider the cardinality constraints on the sets of locations $\llbracket X \rrbracket_{(s, \Sigma)}$ that appear in decorated predicate atoms $p_{I,J,\sim,\ne}(\vec{x}, X)$. The cardinalities of these sets are constrained by the (decorated) predicate's rules. These constraints are essential for satisfiability checking. For instance, as observed in the introduction, the formula $\mathbf{ls}_{\text{even}}(x, Y) \oplus \mathbf{ls}_{\text{odd}}(x, Y)$ is unsatisfiable if $\mathbf{ls}_{\text{even}}$ and $\mathbf{ls}_{\text{odd}}$ describe lists of even and odd lengths respectively, and $Y$ is defined in both cases to collect the set of locations allocated by each list. We show that the cardinality constraints induced by each decorated predicate atom can be encoded, in linear time, as an existential Presburger formula. To achieve this, we rely on known results [23] about the Presburger encoding of Parikh images of context-free languages.

**Definition 16 (Cardinality of a decorated atom).** Let $p_{I,J,\sim,\ne}(\vec{x}, X)$ be a decorated predicate atom of $(\psi, \mathcal{R}_{\text{dec}})$. The cardinality set of $p_{I,J,\sim,\ne}(\vec{x}, X)$, which is denoted by $Sp(p_{I,J,\sim,\ne}(\vec{x}, X))$, is defined by:

$$Sp(p_{I,J,\sim,\ne}(\vec{x}, X)) = \{\text{card}(\Sigma(X)) \mid \exists(s, b, \Sigma). (s, b, \Sigma) \models_{\mathcal{R}_{\text{dec}}} p_{I,J,\sim,\ne}(\vec{x}, X)\}, \quad (14)$$

i.e., it is a (possible unbounded) subset of $\mathbb{N}$, which collects the cardinalities of $X$ for each structure satisfying $p_{I,J,\sim,\ne}(\vec{x}, X)$.

It is straightforward to show that $Sp(p_{I,J,\sim,\ne}(\vec{x}, X)) = Sp(p_{I,J,\sim,\ne}(\vec{x}, X)\sigma)$, for every renaming $\sigma$. In the following, we show that $Sp(p_{I,J,\sim,\ne}(\vec{x}, X))$ is a semi-linear set that can be encoded using an existential Presburger formula with one free variable. To this end, we define a context-free grammar for the predicate atom $p_{I,J,\sim,\ne}(\vec{x}, X)$ using the rules of $\mathcal{R}_{\text{dec}}$, such that the language of this grammar encodes the elements of $Sp(p_{I,J,\sim,\ne}(\vec{x}, X))$ in unary. The idea is to associate each predicate atom with a non-terminal of the grammar, and to associate each rule used in the unfolding with a production rule of the grammar. The set of non-terminals is finite because the set of predicate atoms is finite up to a renaming of parameters. The context-free grammar for $p_{I,J,\sim,\ne}(\vec{x}, X)$ is defined as follows.

**Definition 17 (Grammar of cardinalities).** Let $\mathcal{R}_{\text{dec}}$ be a decorated SID. Let $a \mapsto N_a$ be any mapping from decorated atoms to symbols, such that $N_a = N_b$ iff a and b are identical up to a renaming. The grammar of cardinalities for the decorated atom $p_{I,J,\sim,\ne}(\vec{x}, X)$ is a context-free grammar $G_{p_{I,J,\sim,\ne}(\vec{x}, X)} = (\mathcal{N}, \mathcal{T}, \mathcal{R}, N_0)$ where

- the set of terminals $\mathcal{T}$ is the singleton set $\{1\}$;

- the set of non-terminals $\mathcal{N}$ contains a non-terminal $N_{q_{K,L,\sim,\ne}(\vec{y}, Y)}$ for each decorated predicate atom $q_{K,L,\sim,\ne}(\vec{y}, Y)$ (up to a renaming);

- the start symbol $N_0$ is $N_{p_{I,J,\sim,\ne}(\vec{x}, X)}$;

- the set of derivation rules $\mathcal{R}$ contains a rule of the form

$$N_{q_{K,L,\sim,\ne}(\vec{y}, Y)} \to \omega N_{r_{K_1,L_1,\sim,\ne_1}^1(\vec{y}_1, Y_1)} \cdots N_{r_{K_m,L_m,\sim,\ne_m}^m(\vec{y}_m, Y_m)}, \quad (15)$$

for all formulae $\psi$ such that $q_{K,L,\sim,\ne}(\vec{y}, Y) \Leftarrow_{\mathcal{R}_{\text{dec}}} \psi$ where:
• $\psi$ is of the form $y_j.f \to (\vec{z}) \star \star_{i=1}^{m} r_{K_i, L_i, \sim_{i} \neq i}^{j} (\vec{Y}_i, Y_i) \star \varphi \star Y \approx E \sqcup \sqcup_{i=1}^{m} Y_i;$

• $\omega = 1$ if $E = \{y_j\}$, otherwise (i.e., if $E = \emptyset$) $\omega$ is the empty word $\varepsilon$.

We denote by $L(G)$ the language of words generated by the grammar $G$.

The Parikh image [19] of a word $\omega = \omega_1 \cdots \omega_k \in \mathcal{T}^*$ is the assignment $\sigma \in \mathbb{N}^{|\mathcal{T}|}$ that maps each symbol $a \in \mathcal{T}$ to the number of its occurrences in $\omega$, i.e., $\sigma(a) = \text{card}(j | a = \omega_j)$. The Parikh image of a set $L \subseteq \mathcal{T}^*$ is the set of Parikh images of all $\omega \in L$. If a language $L$ is generated by a context-free grammar $G$, then the Parikh image of $L$ can be represented by an existential Presburger formula $\xi_G$, which can be computed in linear time, by [23, Th. 4]. The formula $\xi_G$ contains one free variable for each terminal symbol of $G$. We shall prove later that the Parikh image of the language defined by $G_{p_{I,J,\sim,\neq}(\vec{x},X)}$ is exactly the cardinality set $Sp(p_{I,J,\sim,\neq}(\vec{x},X))$. Since the grammar of cardinalities $G = G_{p_{I,J,\sim,\neq}(\vec{x},X)}$ has only one terminal, the formula $\xi_G$ contains exactly one free variable and its size is in $O(|\mathcal{N}| + |\mathcal{R}| \cdot |\mathcal{R}|)$ where $\mathcal{N}$ and $\mathcal{R}$ are (respectively) the set of non-terminals and productions of $G_{p_{I,J,\sim,\neq}(\vec{x},X)}$. To simplify notations, we shall denote by $\xi_{p_{I,J,\sim,\neq}(\vec{x},X)}$ the formula $\xi_G$ with $G = G_{p_{I,J,\sim,\neq}(\vec{x},X)}$, and by $\xi_{p_{I,J,\sim,\neq}(\vec{x},X)}(y)$ the formula obtained by replacing the unique free variable in $\xi_G$ by $y$.

**Remark 3.** A smaller Presburger formula for $Sp(p_{I,J,\sim,\neq}(\vec{x},X))$ may be obtained by translating $\mathcal{R}_{dec}$ into a NFA over a singleton alphabet and by using the result of [22]. The resulting formula, obtained in polynomial time, does not contain universal quantifiers and its size is linear in the size of the NFA. We choose to use context-free grammars and the result in [23] in order to simplify the proof of correctness.

### 3.3 Translation from SL to BAPA

The syntax of BAPA formulæ is recalled below, with definitions slightly adapted for consistency with those of OSL<fnref n="5" />.

**Definition 18 (BAPA formulæ [11]).** The set of BAPA-formulæ $\varphi^{BP}$ is inductively defined as follows:

$$
\begin{align*}
\varphi^{BP} &:= A^{BP} \mid B^{BP} \mid \varphi_1^{BP} \wedge \varphi_2^{BP} \mid \varphi_1^{BP} \vee \varphi_2^{BP} \mid \neg \varphi^{BP} \mid \exists X. \varphi^{BP} \mid \forall X. \varphi^{BP} \mid \exists k. \varphi^{BP} \mid \forall k. \varphi^{BP} \\
A^{BP} &:= t_1^{BP} \approx_{BP} t_2^{BP} \mid t_1^{BP} <_{BP} t_2^{BP} \mid K \text{ div } t^{BP} \quad t^{BP} := k \quad K \quad t_1^{BP} \oplus_{BP} t_2^{BP} \quad K \odot_{BP} t^{BP} \quad |T^{BP}| \\
B^{BP} &:= T_1^{BP} \approx_{BP} T_2^{BP} \mid T_1^{BP} \subseteq_{BP} T_2^{BP} \quad T^{BP} := X \mid \emptyset \mid T_1^{BP} \sqcup_{BP} T_2^{BP} \mid T_1^{BP} \sqcap_{BP} T_2^{BP} \tag{16}
\end{align*}
$$

where $X$ is a set variable, $K$ is an integer constant, and $k$ is an integer variable.

**Definition 19 (BAPA structure).** A BAPA structure is a tuple $(\mathcal{S}, \mathcal{I})$ where $\mathcal{S}$ is an interpretation of the set variables, i.e., a partial function from set variables to finite subsets $\mathcal{L}$, and $\mathcal{I}$ is an interpretation of the integer variables, i.e., a partial function from integer variables to $\mathbb{Z}$.

The semantics of BAPA terms and formulæ are the expected ones.

<footnote n="5">⁵ Specifically, instead of assuming a finite universe, we interpret set variables as finite subsets of $\mathcal{L}$, and omit all BAPA terms that depend on the universe, such as the complement operation.</footnote>
**Definition 20.** The function $\mathcal{T}^f$ maps a decorated symbolic heap formula in OSL to a BAPA term containing all (named) locations allocated by a field $f \in \mathcal{F}$. It is defined inductively as follows (where L, A and B denote pure atoms, defined as in Definition 1):

$$- \mathcal{T}^f(\mathbf{emp}) = \mathcal{T}^f(L) = \mathcal{T}^f(A) = \mathcal{T}^f(B) = \emptyset;$$

$$- \mathcal{T}^f(x.g \to (y_1, \dots, y_d)) = \begin{cases} V_x & \text{if } g = f \\ \emptyset & \text{otherwise} \end{cases};$$

$$- \mathcal{T}^f(p_{I,J,\sim,\ne}(x_1, \dots, x_n, X)) = \begin{cases} X \sqcup_{BP} (\sqcup_{j \in J}^{BP} V_{x_j}) & \text{if } p \text{ is a } \{f\}\text{-predicate} \\ \emptyset & \text{otherwise} \end{cases};$$

$$- \mathcal{T}^f(\psi_1 \bullet \psi_2) = \mathcal{T}^f(\psi_1) \cup \mathcal{T}^f(\psi_2) \text{ for } \bullet \in \{\star, \oplus\}.$$

**Definition 21 (BAPA translation function).** Let $X \mapsto i_X$ be an injective function mapping every set variable to an integer variable (which is intended to denote the cardinality of the set). The function $\mathcal{T}$ translates a set term in $\mathfrak{T}$ into a BAPA set term and a decorated symbolic heap formula into a BAPA formula, given a decorated SID $\mathcal{R}_{dec}$ (which, to simplify notations, is considered fixed in the context):

$$- \mathcal{T}(\{x\}) = V_x; \mathcal{T}(X) = X \text{ if } X \in \mathcal{S}; \mathcal{T}(\emptyset) = \emptyset; \mathcal{T}(t) = t \text{ if } t \text{ is an arithmetic term};$$

$$- \mathcal{T}(\mathbf{emp}) = \text{true}; \mathcal{T}(x.f \to (y_1, \dots, y_d)) = \text{true};$$

$$- \mathcal{T}(x \approx y) = (V_x \approx_{BP} V_y); \mathcal{T}(x \neq y) = (V_x \sqcap_{BP} V_y \approx_{BP} \emptyset);$$

$$- \mathcal{T}(T_1 \approx T_2) = (\mathcal{T}(T_1) \approx_{BP} \mathcal{T}(T_2)); \text{ the definition is similar for } \sqcup, \sqcap, \subseteq \text{ or } <;$$

$$- \mathcal{T}(T_1 \not\approx T_2) = \neg(\mathcal{T}(T_1) \approx_{BP} \mathcal{T}(T_2)); \text{ the definition is similar for } \not\sqcup \text{ or } \not<;$$

$$- \mathcal{T}(K \text{ div } t) = (K \text{ div } \mathcal{T}(t)); \mathcal{T}(K \text{ ndiv } t) = \neg(K \text{ div } \mathcal{T}(t));$$

$$- \mathcal{T}(p_{I,J,\sim,\ne}(x_1, \dots, x_n, X)) = |X| \approx_{BP} i_X \wedge \xi_{p_{I,J,\sim,\ne}(x_1, \dots, x_n, X)}(i_X) \\ \wedge (\sqcup_{i \in I}^{BP} V_{x_i}) \subseteq_{BP} X \\ \wedge (\sqcup_{x \in \{x_1, \dots, x_n\} \setminus \{x_j \mid j \in I\}}^{BP} V_x) \sqcap_{BP} X \approx_{BP} \emptyset;$$

where the formula $\xi_{p_{I,J,\sim,\ne}(x_1, \dots, x_n, X)}$ is defined as in Sect. 3.2.

$$- \mathcal{T}(\psi_1 \star \psi_2) = \mathcal{T}(\psi_1) \wedge \mathcal{T}(\psi_2) \wedge \left( \bigcap_{f \in \mathcal{F}}^{BP} \mathcal{T}^f(\psi_1) \right) \sqcap_{BP} \left( \bigcap_{f \in \mathcal{F}}^{BP} \mathcal{T}^f(\psi_2) \right) \approx_{BP} \emptyset;$$

$$- \mathcal{T}(\psi_1 \oplus \psi_2) = \mathcal{T}(\psi_1) \wedge \mathcal{T}(\psi_2) \wedge \bigwedge_{f \in \mathcal{F}} (\mathcal{T}^f(\psi_1) \sqcap_{BP} \mathcal{T}^f(\psi_2) \approx_{BP} \emptyset).$$

**Proposition 1.** Let $T \in \mathfrak{T} \cup t$ be a set term or an arithmetic term. Let $(s, b, \Sigma)$ be an OSL structure. Let $\mathbb{S}$ be defined by $\mathbb{S}(V_x) = \{s(x)\}$ for all location variables $x$, and $\mathbb{S}(X) = \Sigma(X)$ for all set variables $X$. Then, for every interpretation $\mathcal{I}, \llbracket T \rrbracket_{(s,\Sigma)} = \llbracket \mathcal{T}(T) \rrbracket_{(\mathbb{S},\mathcal{I})}$.

*Proof.* The proof is by induction on $T$ and $t$.

For each decorated symbolic heap $\psi$ in normal form containing location variables $x_1, \dots, x_n$, we associate the following BAPA formula called $C(\psi)$:

$$C(\psi) = |V_{x_1}| \approx_{BP} 1 \wedge \dots \wedge |V_{x_n}| \approx_{BP} 1 \wedge \mathcal{T}(\psi). \qquad (17)$$
**Example 4.** Let us consider the decorated formula $\psi = p_{I,J,\sim,\ne}(x,y,z,X) \star y \nsim z \star z.f \to (x,y)$ taken from Example 3 with $I = \{2\}, J = \{2\}, \sim = \text{Id}, \text{ and } \ne = \emptyset$.

Then the BAPA formula obtained is:

$$ C(\psi) = |V_x| \approx_{BP} 1 \wedge |V_y| \approx_{BP} 1 \wedge |V_z| \approx_{BP} 1 \wedge |X| \approx_{BP} i_X \wedge \xi_{p_{I,J,\sim,\ne}(x,y,z,X)}(i_X) \\ \wedge V_y \sqsubseteq_{BP} X \wedge (V_x \sqcup_{BP} V_z) \sqcap_{BP} X \approx_{BP} \emptyset \wedge V_y \sqcap_{BP} V_z \approx_{BP} \emptyset \wedge \text{true} \\ \wedge (X \sqcup_{BP} V_y) \sqcap_{BP} V_z \approx_{BP} \emptyset. \tag{18} $$

It is straightforward to verify that, for all decorations $\psi$ of a formula $\varphi$, $C(\psi)$ is an existentially quantified BAPA formula. This translation allows us to establish the decidability of the satisfiability problem for a decorated symbolic heap:

**Theorem 3.** Let $(\varphi, \mathcal{R})$ an OSL-formula and a SID in normal form. For all decorations $(\psi, \mathcal{R}_{\text{dec}})$ of $(\varphi, \mathcal{R})$, $\psi$ has an $\mathcal{R}_{\text{dec}}$-model iff $C(\psi)$ is satisfiable (in BAPA).

Theorem 1 then follows directly from Theorems 2 and 3. The NEXPTIME upper bound is obtained by observing that the size of the decorated, normalized set of rules is exponential in the size of the original SID, since the number of possible decorations and instantiations is exponential. Moreover, it is shown in [13] that satisfiability for existentially quantified BAPA formulæ is in Np.

# 4 Conclusion

We have developed a decision procedure to test the satisfiability of formulæ in a variant of separation logic (SL) that integrates inductively defined predicate symbols, overlaid data structures, set constraints, and Presburger arithmetic constraints on set cardinals. This fragment, designed to address the limitations of standard SL in reasoning about overlaid data structures, uses a weaker form of separating conjunction and supports single-field inductive predicates augmented with set variables. Our procedure operates in exponential space, leveraging established results on the computation of the Parikh image of context-free languages over a unary alphabet and the satisfiability problem in the logic BAPA. This reduction yields a robust framework for handling complex memory models occurring in concurrent systems and advanced algorithmic designs, where locations may be shared across multiple data structures.

A natural extension of this work is to explore the entailment problem. Given the undecidability of entailment in many expressive SL variants (see for instance [5,20]), additional restrictions will be required to ensure decidability. Several questions also remain unresolved regarding satisfiability. First, the optimality of our procedure is uncertain: while satisfiability is clearly EXPTIME-hard$^6$, it is not clear whether NEXPTIME represents a tight upper bound. Second, it would be valuable to investigate whether the systematic enumeration of all decorations could be circumvented. This process currently incurs an exponential computational overhead, which does not affect the theoretical complexity analysis but poses practical challenges. Finally, it would be interesting to determine whether the conditions on the inductive rules could be relaxed. For instance, is satisfiability still decidable if a single predicate is permitted to allocate distinct fields?

<footnote>$^6$ This follows from the lower bound given in [20], since that result does not use permissions and imposes strictly more restrictive conditions on the rules.</footnote>
## References

1. Berdine, J., Calcagno, C., O'Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005). https://doi.org/10.1007/11575467_5

2. Brotherston, J., Fuhs, C., Pérez, J.A.N., Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, pp. 1–10. Association for Computing Machinery, New York (2014). https://doi.org/10.1145/2603088.2603091

3. Drăgoi, C., Enea, C., Sighireanu, M.: Local shape analysis for overlaid data structures. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 150–171. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_10

4. Echenim, M., Iosif, R., Peltier, N.: Decidable entailments in separation logic with inductive definitions: beyond establishment. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, vol. 183, pp. 20:1–20:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.CSL.2021.20

5. Echenim, M., Iosif, R., Peltier, N.: Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules. Inf. Process. Lett. 173, 106169 (2022). https://doi.org/10.1016/j.ipl.2021.106169

6. Enea, C., Saveluc, V., Sighireanu, M.: Compositional invariant checking for overlaid and nested linked lists. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 129–148. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-9_6

7. Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 532–549. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_36

8. Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 21–38. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_2

9. Ishtiaq, S.S., O'Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001, pp. 14–26. Association for Computing Machinery, New York (2001). https://doi.org/10.1145/360204.375719

10. Krishna, S., Shasha, D., Wies, T.: Go with the flow: compositional abstractions for concurrent data structures. Proc. ACM Program. Lang. 2(POPL), 37:1–37:31 (2017). https://doi.org/10.1145/3158125

11. Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 260–277. Springer, Heidelberg (2005). https://doi.org/10.1007/11532231_20

12. Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean algebra with presburger arithmetic. J. Autom. Reason. 36(3), 213–239 (2006). https://doi.org/10.1007/s10817-006-9042-1

13. Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_15

14. Le, Q.L., Le, X.B.D.: An efficient cyclic entailment procedure in a fragment of separation logic. In: Kupferman, O., Sobocinski, P. (eds.) FoSSaCS 2023. LNCS, vol. 13992, pp. 477–497. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30829-1_23
15. Lee, O., Yang, H., Petersen, R.: Program analysis for overlaid data structures. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 592–608. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_48

16. Lee, O., Yang, H., Petersen, R.: A divide-and-conquer approach for analysing overlaid data structures. Formal Methods Syst. Des. 41(1), 4–24 (2012). https://doi.org/10.1007/s10703-012-0151-7

17. Matheja, C., Pagel, J., Zuleger, F.: A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. ACM Trans. Comput. Logic 24(1), 1:1–1:76 (2023). https://doi.org/10.1145/3534927

18. Meyer, R., Wies, T., Wolff, S.: Make flows small again: revisiting the flow framework. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 628–646. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30823-9_32

19. Parikh, R.J.: On context-free languages. J. ACM 13(4), 570–581 (1966). https://doi.org/10.1145/321356.321364

20. Peltier, N.: Testing the satisfiability of formulas in separation logic with permissions. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNCS, vol. 14278, pp. 427–445. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-43513-3_23

21. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, pp. 55–74 (2002). https://doi.org/10.1109/LICS.2002.1029817. ISSN 1043-6871

22. Sawa, Z.: Efficient construction of semilinear representations of languages accepted by unary nondeterministic finite automata. Fundamenta Informaticae 123(1), 97–106 (2013). https://doi.org/10.3233/FI-2013-802

23. Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 337–352. Springer, Heidelberg (2005). https://doi.org/10.1007/11532231_25

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

<figure><img src="image_20.png" /></figure>
# Subtyping in Dependently-Typed
Higher-Order Logic

Colin Rothgang$^{1,2(✉)}$ and Florian Rabe$^{3(✉)}$

¹ Imdea Software Institute, Madrid, Spain
[colin.rothgang@posteo.net](mailto:colin.rothgang@posteo.net)

² Universidad Politécnica de Madrid, Madrid, Spain

³ Computer Science, FAU Erlangen-Nürnberg, Erlangen, Germany

**Abstract.** The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its expressiveness over standard HOL. Yet it retains strong automated theorem proving support via a sound and complete translation to HOL.

We leverage this design to extend DHOL with refinement and quotient types. Both of these are commonly requested by practitioners but rarely provided by automated theorem provers. This is because they inherently require undecidable typing and thus are very difficult to retrofit to decidable type systems. But with DHOL already doing the heavy lifting, adding them is not only possible but elegant and simple.

Concretely, we add refinement and quotient types as special cases of subtyping. This turns the associated canonical inclusion resp. projection maps into identity maps and thus avoids costly changes in representation. We present the syntax, semantics, and translation to HOL for the extended language, including the proofs of soundness and completeness.

## 1 Introduction and Related Work

*Motivation.* Recently dependently typed higher-order logic (DHOL) was introduced [22]. It is a variant of HOL [2,6] that uses dependent function types $Πx:A. B$ instead of simple function types $A \to B$. It is designed to remain as simple and as close to HOL and ATPs as possible while meeting the frequent user demand of dependent types. Notably, contrary to typical formulations of dependent type theory, DHOL features a straightforward equality and classical Booleans at the cost of making typing undecidable.

Concretely, DHOL uses a type *bool* of propositions in the style of HOL, and equality $s =_A t$: *bool* of typed terms is a proposition, whose truth may depend on axioms in the theory or assumptions in the context. Equality $A \equiv B$ of types (which is not a proposition but a meta-level judgment) uses a straightforward congruence rule: if a dependent type constructor is applied to equal arguments, it produces equal types. Thus, equality of types and typing are undecidable. To yield practical tool support, DHOL reduces typing judgments to a series of proof
obligations, and [22] gives a sound and complete translation to HOL that allows using existing automated theorem provers for HOL to discharge these.

While undecidable typing is not used by most current ATPs or ITPs, it is justified by the pragmatic consideration that the ultimate task of theorem proving is undecidable anyway, and the difficulty of typing-related proof obligations is often small in comparison. Follow-up work on DHOL includes a native ATP for DHOL [17] and extensions with a choice operator [20] and polymorphism [21].

**Contribution.** The present paper leverages this key design choice and extends DHOL's expressivity at low cost by adding refinement and quotient types. Both work elegantly in languages with undecidable typing so that DHOL, for which the necessary meta-theory and infrastructure already exist, is a good base to support them. Indeed, the necessary changes to DHOL's syntax and semantics turned out to be few and simple—only the extension of the proof was difficult. We see DHOL as an intermediate between the automation support of HOL and the more expressive type theories of interactive provers such as those based on richer dependent type theories. In this sense, the present paper pushes the boundary of ATP-near languages a little further.

**Refinement types** $A|_p$ is the subtype of $A$ consisting of the terms satisfying the predicate $p:A \to \mathbf{bool}$. They correspond to comprehension in set theory. They were already proposed in [22] (with ad-hoc subtyping rules), and here we give a systematic treatment. Critically, our refinement types avoid a change in representation: the injection $A|_p \to A$ is always a no-op, i.e., an identity map. This is in contrast to encodings of refinement types in decidable type theories, such as using the type $\Sigma x:A.p x$, or in set-theory, where, e.g., the injection $(A \to B) \to (A|_p \to B)$ is not a no-op.

**Quotient types** $A/r$, intuitively, consist of all equivalence classes of the equivalence relation $r:A \to A \to \mathbf{bool}$. Again we avoid representation changes: We use all terms of type $A$ as terms of type $A/r$ and adjust the equality $=_{A/r}$ to obtain the quotient semantics. Thus, the projection $A \to A/r$ is a no-op and we have the subtyping relation $A \prec: A/r$. In contrast, the usual definitions in set theory (via equivalence classes) or in decidable type theories (via setoids) require explicit changes in representation.

The statement $A \prec: A/r$ may look odd. It is sound because we use a different equality relation at the two types: $x=A y$ implies $x=A/r y$ but not the other way round. This approach captures the mathematical practice of using elements of $A$ as elements of the quotient, often to the point that readers do not even notice anymore they are technically working with equivalence classes.

Together, this yields a subtype hierarchy of refinements and quotients of $A$: $A|_{\lambda x:A. \mathbf{false}} \prec: \mathbf{.:A}|_p \prec: \mathbf{.:A}|_{\lambda x:A. \mathbf{true}} \equiv A \equiv A/=_{A} \prec: \mathbf{.:A}/r \prec: \mathbf{.:A}/\lambda x, y:A. \mathbf{true}$ from initial (empty) type to terminal (singleton) type.

**Related Work.** Systems based on HOL [11] use the subtype definition principle to introduce definitional refinement types. General refinement types in HOL were
considered in [15]. But neither solution has a general notion of subtyping. Definitional quotient types for HOL were considered in [12] and [13] and, combined with refinement types, in [19]. Definitional solutions differ from ours in that they introduce new types that are isomorphic to the refinement/quotient types and then require explicit representation-changing injection/projections. [19] uses PERs to relativize type-based to set-based theorems.

In formal systems, the approach of quotients as supertypes has been adopted occasionally, e.g., in NuPRL's quotients [7] or in Quotient Haskell [3]. NuPRL's type theory in particular features refinement and quotient types similar to ours and uses essentially the same PER semantics [1]. The main difference to our approach is that DHOL tries to be as close to HOL (and thus HOL ATPs) as possible whereas NuPRL uses a very rich type theory.

PVS [18] subsumes DHOL and refinement types with polymorphism. It does not support quotients, but its horizontal subtyping between records resembles our quotient subtyping. Notably, it treats refinement subtyping and record subtyping as two separate judgments with slightly different rules.

In soft type systems, all types are refinements of a fixed universe of objects. For example, Mizar's [4] type system is inherently undecidable and supports dependent types and refinement types. It supports quotient types but only with a change in representation and not as supertypes.

Most ITPs allow users to construct refinement and quotient types at the cost of representation changes. Systems based on decidable dependent type theory like Coq [8] or Lean [9] typically use $\Sigma$-types for refinement and setoids for quotients. Lean provides some kernel support for quotients.

[21] adds polymorphism to DHOL, and in future work we want to combine both features. The key challenge will be to support subtype-bounded polymorphism.

*Overview.* We give a self-contained definition of DHOL in Sect. 2. Then we add subtyping in Sect. 3, refinements in Sect. 4, and quotients in Sect. 5. We develop the meta-theory in Sect. 6 (type normalization) and Sect. 7 (soundness/completeness). We present an application to typed set theory in Sect. 8.

## 2 Preliminaries: Dependently Typed Higher-Order Logic

The DHOL [22] grammar uses terms and types. A theory $T$ declares typed constants $c:A$, axioms $\triangleright F$, and dependent type symbols $a:\Pi x_1:A_1...\Pi x_n:A_n$. tp, which are applied to terms to obtain base types $a t_1 ... t_n$. Contexts declare typed variables $x:A$ and local assumptions $\triangleright F$ (but no new types). Dependent functions $\lambda x:A. t$ of type $\Pi x:A. B$ (written $A \to B$ if $x$ does not occur free in $B$) map terms $x:A$ to terms of type $B(x)$. We recover HOL as the fragment in which all base types $a$ have arity 0, in which case all function types are simple.

<table><tr><td>T</td><td>::=</td><td>o | T, a:(Πx:A.)* tp | T, c:A | T, ▷F</td><td>theories</td></tr><tr><td>Γ</td><td>::=</td><td>· | Γ, x:A | Γ, ▷F</td><td>contexts</td></tr><tr><td>A, B</td><td>::=</td><td>a t* | Πx:A. B | bool</td><td>types</td></tr><tr><td>s, t, F, G</td><td>::=</td><td>c | x | λx:A. t | s t | s =<sub>A</sub> t | F ⇒ G</td><td>terms (incl. propositions)</td></tr></table>
Following typical HOL-style [2], DHOL defines all connectives and quantifiers from the equality connective $s =_A t$. For example,forall is defined as $\forall x:A. F := \lambda x:A. F = \Pi x:A. \mathbf{bool} \lambda x:A. \mathbf{true}$. In particular, we can define the usual connectives and quantifiers and derive their usual proof rules. The only subtlety is that, DHOL needs *dependent binary connectives*: in an implication $F \Rightarrow G$, the well-formedness of $G$ may depend on the truth of $F$, and accordingly for conjunction $F \land G$ which is defined as $\neg(F \Rightarrow \neg G)$. Because we see no way to define these from equality, we make dependent implication an additional primitive.

DHOL uses axiomatic equality $s =_A t$ in the style of FOL and HOL with a straightforward congruence rule for base types: type equality a $s_1$ ... $s_n \equiv$ a $t_1$ ... $t_n$ holds if each $s_i$ is equal to $t_i$. This makes type equality and thus typing undecidable. In line with HOL's simplicity and unlike dependent type theories based on Martin-Löf type theory [16], there is no support for type-valued computation like large elimination.

*Example 1 (Lists)*. As an accessible running example, we show a formalization of lists over some type *obj*, both plain lists *list* and lists *llist* *n* with fixed length. Notably, the well-typedness of the statement of associativity of *lconc* now requires the associativity of *plus*.

nat: tp, zero: nat, succ: nat $\rightarrow$ nat, plus: nat $\rightarrow$ nat $\rightarrow$ nat,

obj: tp, list: tp, nil: list, cons: obj $\rightarrow$ list $\rightarrow$ list, conc: list $\rightarrow$ list $\rightarrow$ list,

llist: nat $\rightarrow$ tp, lnil: llist zero,

lcons: $\Pi n:nat. obj \rightarrow llist n \rightarrow llist$ (succ $n$),

lconc: $\Pi m,n:nat. llist m \rightarrow llist n \rightarrow llist$ (plus $m$ $n$)

<table><caption>**Fig. 1.** DHOL Judgments</caption><thead><tr><th>Name</th><th>Judgment</th><th>Intuition</th></tr></thead><tbody><tr><td>theories</td><td>$\vdash_T$ Thy</td><td>$T$ is a well-formed theory</td></tr><tr><td>contexts</td><td>$\vdash_T$ $\Gamma$ Ctx</td><td>$\Gamma$ is a well-formed context</td></tr><tr><td>types</td><td>$\Gamma \vdash_T$ A tp</td><td>A is a well-formed type</td></tr><tr><td>typing</td><td>$\Gamma \vdash_T$ t:A</td><td>t is a well-formed term of well-formed type A</td></tr><tr><td>validity</td><td>$\Gamma \vdash_T$ F</td><td>well-formed Boolean F is derivable</td></tr><tr><td>equality of types</td><td>$\Gamma \vdash_T$ A $\equiv$ B</td><td>well-formed types A and B are equal</td></tr></tbody></table>

DHOL uses the **judgments** given in Fig. 1 and the **rules** listed in Fig. 2. Note that equality of terms is a special case of validity, whereas equality of types is not a Boolean but a separate judgment. Thus, users cannot state axioms equating types, and type equality is defined only by congruence. The rules are straightforward. In particular, type equality is checked structurally and reduced to a set of term equalities, which must then be discharged by an ATP.
Theories and contexts:

<figure><img src="image_21.png" /></figure>

Well-formedness and equality of types:

<figure><img src="image_22.png" /></figure>

Typing:

<figure><img src="image_23.png" /></figure>

Equality: congruence, reflexivity, symmetry, $\beta$, $\eta$ (transitivity and extensionality are derivable):

<figure><img src="image_24.png" /></figure>

Rules for validity: lookup, implication, Boolean equality and Boolean extensionality:

<figure><img src="image_25.png" /><figcaption>Fig. 2. DHOL Rules</figcaption></figure>

<figure><img src="image_26.png" /></figure>

<table><caption>Fig. 3. Definition of the Translation DHOL→HOL</caption><thead><tr><th>if in DHOL</th><th>then in HOL</th></tr></thead><tbody><tr><td>type A</td><td>type A and PER A*:A → A → bool</td></tr><tr><td>term t:A</td><td>term t:A satisfying A* t t</td></tr></tbody></table>
Furthermore many well-known admissible HOL rules are also admissible in DHOL, see the extended preprint [5].

The semantics for DHOL and a practical ATP workflow are given by a sound and complete translation to HOL. The translation is dependency era- sure, e.g., translating dependent types a $t_1 ... t_n$ to simple types a, effectively “merging” all instances of a dependent type into a large simple type. Figure 3 shows the details.

Typing and equality at $A$ are recovered by generating a partial equivalence relation (PER) $A^*$ for every HOL-type $\bar{A}$. A PER is a symmetric-transitive relation and the same as an equivalence relation on a subtype of $\bar{A}$. Thus, $A$ corresponds in HOL to the quotient of the appropriate subtype of $\bar{A}$ by $A^*$.

DHOL terms are translated to their HOL analogues except that equality is translated to the respective PER: $s =_A \bar{t} := A^* \bar{s} \bar{t}$. In particular, the predicate $A^* \bar{t} \bar{t}$ captures whether $t$ is a term of type $A$. For $n$-ary type symbols $a$, the translation generates an $n+2$-ary predicate $a^*$ such that $a^* \bar{t}_1 ... \bar{t}_n$ is the PER for a $t_1 ... t_n$. For function types, the PER is the usual condition for logical relations: functions are related if they map related inputs to related outputs.

## 3 Subtyping

The treatment of quotients as supertypes and the use of different equality relations at different types are subtly difficult. Thus, we first introduce subtyping by its defining extensional property, from which we will derive all subtyping rules:

**Definition 1 (Subtyping).** $\Gamma \vdash_T A \prec B$ abbreviates $\Gamma, x:A \vdash_T x:B$.

**Lemma 1.** In any extension of DHOL, $\Gamma \vdash_T A \prec B$ iff $\frac{\Gamma \vdash_T t:A}{\Gamma \vdash_T t:B}$ is derivable.

*Proof.* Left-to-right: We construct the function $(\lambda x:A. x):A \to B$ and derive the desired rule using the typing rule for function application.
Right-to-left: We start with $\Gamma, x:A \vdash_T x:A$ and apply the derivable rule.

This subtyping relation prevents *incidental* subtype instances, for which the rule from Lemma 1 is admissible but not derivable. For example, $A|_{\lambda x:A. \text{false}}$ is a subtype of all refinements of $A$, but not of all types. More generally, this definition precludes using induction on the terms of $A$ to conclude $A \prec B$. This restriction ensures that subtyping is preserved under, e.g., theory extensions, substitution, or language extensions. Importantly, subtyping preserves equality:

**Lemma 2.** *Consider some extension of DHOL with productions and rules. Assume (*) that $\Gamma \vdash_T x =_B x$ implies $\Gamma \vdash_T x : B$. Let $F := \forall x:A. \forall y:A. x =_A y \Rightarrow x =_B y$. Then $\Gamma \vdash_T A \prec B$ iff $\Gamma \vdash_T F : \text{bool}$; and if these hold, then also $\Gamma \vdash_T F$.*

<footnote>(*) is a very mild assumption and satisfied by all extensions given in this paper.</footnote>
### Proof.

Left-to-right: The assumption yields $\Gamma, x:A, y:A, \triangleright x =_A y \vdash_T (\lambda x:A. x):A \to B$. We get $\Gamma, x:A, y:A, \triangleright x =_A y \vdash_T (\lambda x:A. x) x =_B (\lambda x:A. x) y$ from congruence of function application and reflexivity and $x =_B y$ by $\beta$-reduction.

Right-to-left: Assume $x : A$. Instantiating $\Gamma$ twice with $x$ and applying modus ponens with $x =_A x$ yields $x =_B x$, from which we get $x : B$.

**Lemma 3 (Preorder of Types).** In any extension of DHOL, subtyping is reflexive (in the sense that $\Gamma \vdash_T A \equiv B$ implies $\Gamma \vdash_T A \prec : B$) and transitive.

*Proof.* Reflexivity: The assumption yields $\Gamma \vdash_T (\lambda x:A. x):A \to B$. Applying both to a term $t$ of type $A$ and $\beta$-reducing yields the rule from Lemma 1. Transitivity follows immediately from Lemma 1.

We also want to make subtyping an order. Anti-symmetry with respect to $\equiv$ is not derivable directly, i.e., we might have $\Gamma \vdash_T A \prec : B$ and $\Gamma \vdash_T B \prec : A$, in which case $A$ and $B$ would have the same terms, without being equal. Therefore, we add the anti-symmetry rule

$$ \frac{\Gamma \vdash_T A \prec : B \quad \Gamma \vdash_T B \prec : A}{\Gamma \vdash_T A \equiv B} \qquad \text{STantisym} $$

Notably, this is the only change made to DHOL so far—everything before has just been abbreviations. This change is conservative in the following sense:

**Theorem 1 (Conservativity).** For DHOL as defined so far (without the extension we introduce below), we have $A \prec : B$ iff $A \equiv B$.

*Proof.* We show by induction on derivations that each term has a unique type up to type equality and that all term equality axioms preserve typing.

**Theorem 2 (Variance and Congruence for Function Types).** The usual rules for function types are derivable:

$$ \frac{\Gamma \vdash_T A' \prec : A \quad \Gamma, x:A' \vdash_T B \prec : B'}{\Gamma \vdash_T \Pi x:A. B \prec : \Pi x:A'. B'} \qquad \frac{\Gamma \vdash_T A' \equiv A \quad \Gamma, x:A' \vdash_T B \equiv B'}{\Gamma \vdash_T \Pi x:A. B \equiv \Pi x:A'. B'} $$

The second rule is primitive in DHOL but derivable in DHOL with subtyping.

*Proof.* The first rule follows from the definition of subtyping and $\eta$-expansion. The second rule is derived by (STantisym), establishing the hypotheses using the variance rule and reflexivity of subtyping.
# 4 Refinement Types

To add refinement types, we add only one production for types. We do not add productions for terms—refinement types only provide new typing properties for the existing terms. Then we add rules for, respectively, formation, introduction, elimination (two rules), and equality:

$$A ::= A|_p \quad \text{type A refined by predicate } p \text{ on A}$$

$$\frac{\Gamma \vdash_T p: A \rightarrow \mathbf{bool} \qquad \Gamma \vdash_T t: A \qquad \Gamma \vdash_T p t}{\Gamma \vdash_T A|_p \mathbf{tp}}$$ $$\frac{\Gamma \vdash_T t: A|_p}{\Gamma \vdash_T t: A} \qquad \frac{\Gamma \vdash_T t: A|_p}{\Gamma \vdash_T p t} \qquad \frac{\Gamma \vdash_T s =_A t \qquad \Gamma \vdash_T p s}{\Gamma \vdash_T s =_{A|_p} t}$$

**Example 2 (Refining Lists by Length).** We extend Example 1 by defining fixed-length lists as a refinement of lists. First, we axiomatize a predicate `length` on lists:

$$\begin{array}{l@{\quad}l@{\quad}l}
\text{length: } \mathbf{list} \rightarrow \mathbf{nat} & \triangleright \text{ length } \mathbf{nil} =_{\mathbf{nat}} \mathbf{zero} & \\
\triangleright \forall x:\mathbf{obj}. \forall l:\mathbf{list}. \text{ length } (\text{cons } x \; l) =_{\mathbf{nat}} \text{ succ } (\text{length } l)
\end{array}$$

Then we define `llist n` := `list|$_{\lambda l}$:list. length $l$=$_{nat}$ n, and we can derive

$$\vdash \mathbf{nil}$:llist zero \qquad n: nat \vdash \mathbf{cons} : \Pi x:\mathbf{obj}. \Pi l:llist n. \mathbf{llist} (\mathbf{succ} n)$$

**Theorem 3 (Congruence and Variance).** *The following rules are derivable if the involved types are well-formed:*

$$\frac{\Gamma \vdash_T A \prec: A' \qquad \Gamma, x:A, \triangleright p x \vdash_T p' x}{\Gamma \vdash_T A|_p \prec: A'|_{p'}} \qquad \frac{\Gamma \vdash_T A \mathbf{tp}}{\Gamma \vdash_T A \equiv A|_{\lambda x:A. \text{ true}}}$$ $$\frac{\Gamma \vdash_T A \equiv A' \qquad \Gamma \vdash_T p =_A \mathbf{bool} p'}{\Gamma \vdash_T A|_p \equiv A'|_{p'}} \qquad \frac{\Gamma \vdash_T A|_p \mathbf{tp}}{\Gamma \vdash_T A|_p \prec: A}$$

*Proof.* To derive the first rule, we assume the hypotheses and $x:A|_p$. The elimination rules yield $x:A$ and $p x$, then the hypotheses yield $x:A'$ resp. $p' x$, finally the introduction rule yields $x:A'|_{p'}$.

To derive the second rule, we apply (STantisym) and use the introduction/elimination rules to show the two subtype relationships. These then imply the other rules.
# 5 Quotient Types

To add quotient types we also extend the grammar with only one production for the type and rules for formation, introduction, elimination, and equality, where EqRel($r$) abbreviates that $r$ is an equivalence relation:

$$A ::= A/r \quad \text{quotient of } A \text{ by equivalence relation } r$$

$$\frac{\Gamma \vdash_T A \ \mathrm{tp} \qquad \Gamma \vdash_T r: A \to A \to \mathbf{bool} \qquad \Gamma \vdash_T \mathrm{EqRel}(r)}{\Gamma \vdash_T A/r \ \mathrm{tp}} \qquad \frac{\Gamma \vdash_T t:A \qquad \Gamma \vdash_T A/r \ \mathrm{tp}}{\Gamma \vdash_T t:A/r}$$

$$\frac{\Gamma \vdash_T s:A/r \quad \Gamma, x:A, \triangleright x =_{A/r} s \vdash_T t:B \quad \Gamma, x:A, x':A, \triangleright x =_{A/r} s, \triangleright x' =_{A/r} s \vdash_T t =_B t[x/x']}{\Gamma \vdash_T t[x/s]:B[x/s]}$$

$$\frac{\Gamma \vdash_T s:A \qquad \Gamma \vdash_T t:A \qquad \Gamma \vdash_T r:A \to A \to \mathbf{bool} \qquad \Gamma \vdash_T \mathrm{EqRel}(r)}{\Gamma \vdash_T (s =_{A/r} t) =_{\mathbf{bool}} (r \ \mathrm{s} \ t)}$$

*Example 3 (Sets)*. We extend Example 1 by obtaining sets as a quotient of lists. First, we axiomatize a predicate for containing an element:

$$\begin{array}{l} \text{contains: } \mathbf{list} \to \mathbf{obj} \to \mathbf{bool} \qquad \triangleright \forall x:\mathbf{obj}. \neg(\text{contains } \mathbf{nil} x) \\ \qquad \triangleright \forall x:\mathbf{obj}. \forall y:\mathbf{obj}. \forall l:\mathbf{list}. (\text{contains } (\text{cons } y \ l) x) =_{\mathbf{bool}} (x =_{\mathbf{obj}} y \lor \text{contains } l x) \end{array}$$

Now we can define `set := list/λl:list. λm:list. ∀x:obj. contains l x = bool contains m x` as the type of lists containing the same elements. The equality at `set` immediately yields extensionality `Γ ∀x, y:set. x = set y ⇔ (∀z:obj. contains x z = bool contains y z)`.

Any `l:list` can be used as a representative of the respective equivalence class in `set`, and operations on sets can be defined via operations on lists, e.g., we can establish `Γ conc : set → set → set`. To derive this, we assume `u:set` and apply the elimination rule twice. First we apply it with `B = list → set` and `t = conc u`; we have to show `conc x = list → set` `conc x'` under the assumption that `x` and `x'` are equal as sets. That yields a term `conc u : list → set`. We assume `v:set` and apply the elimination rule again with `B = set` to obtain `conc u v:set`, and then conclude via `λ-abstraction` and `η-reduction`.

The elimination rule above looks overly complex. It can be understood best by comparing it to the following, simpler and more intuitive rule

$$\frac{\Gamma, x:A \vdash_T t:B \qquad \Gamma, x:A, x':A, \triangleright r x x' \vdash_T t =_B t[x/x']}{\Gamma, x:A/r \vdash_T t:B} (*)$$

This rule captures the well-known condition that a function `t` on `A` may be used as a function on `A/r` if `t` maps equivalent representatives `x, x'` equally. It follows from our elimination rule by putting `s = x`, but is subtly weaker:
*Example 4.* Continuing Example 3, assume a total order on `obj` and a function `g: list|nonEmpty` → `obj` picking the maximum from a non-empty list. We should be able to apply `g` to some `s: set` that we know to be non-empty. But if we try to apply `(*)` to obtain `g s: obj`, we get stuck trying to prove `g x = obj g x'` for any `x`, `x'` that are representatives of an arbitrary equivalence class of lists. We cannot use the condition that `s` is non-empty and thus only non-empty lists need to be considered. Thus, we cannot derive the well-formedness of `g x`.

Our elimination rule remedies that: here we need to show $g x = \mathit{obj} g x'$ for any $x, x'$ that are representatives of the class of $s$. Thus, we can use that $x$ and $x'$ are non-empty and that thus $g x$ is well-formed.

In dependent type theory, the two elimination rules are equivalent because we have a type $s = x$ and can use $\Pi s: A/r. s = x \to B$ as the return type. This is not possible in DHOL where $s = x$ is not a type but a Boolean.

**Theorem 4 (Congruence and Variance).** *The following rules are derivable if the involved types are well-formed and $r, r'$ are equivalence relations:*

$$ \frac{\Gamma \vdash_T A \prec A' \qquad \Gamma, x:A, y:A, \triangleright r x y \vdash_T r' x y}{\Gamma \vdash_T A/r \quad A/r \prec A'/r'} \qquad \frac{\Gamma \vdash_T A \mathrm{tp} \qquad \Gamma \vdash_T A \equiv A/\lambda x:A. \lambda y:A. x =_A y}{\Gamma \vdash_T A \prec A' \qquad \Gamma \vdash_T A \equiv A' \qquad \Gamma \vdash_T r =_{A \to A \to \mathbf{bool}} r'} $$

*Proof.* For the first rule: Assume the hypotheses and `s:A/r`. Apply the elimination rule with `B = A'/r'` and `t = x. x:A, y:A, \triangleright x =_{A/r} s, \triangleright x' =_{A/r} s \vdash_T x =_{A'/r'} x'` by the equality rule (using `A \prec A'` and the second assumption). For the second rule, apply (STantisym) and use the introduction/elimination rules to show the two subtype relationships. The other rules follow from those two.

# 6 Normalizing Types

To build a type-checker, we derive normalization rules that reduce subtyping conditions to validity conditions that can then be discharged via an ATP. We prove rules for merging consecutive refinements and quotients and for the 4 possible combinations of a function type with a refinement or quotient:

**Theorem 5 (Repeated Refinement/Quotient).** *The following are derivable whenever the LHS is well-formed*

$$ \vdash_T (A|_p)|_{p'} \equiv A|_{\lambda x:A. p x \land p'} x \qquad (RR) $$

$$ \vdash_T (A/r)|_{r'} \equiv A/\lambda x:A. \lambda y:A. r' x y \qquad (QQ) $$

$$ \vdash_T (A/r)|_p \equiv (A|_p)/r \qquad (RQ) $$
**Proof. (RR):** well-formedness of the LHS yields $p:A \rightarrow \mathbf{bool}$ and $p':A|_p \rightarrow \mathbf{bool}$, so $p'$ $x$ is well-formed as $\wedge$ is a dependent conjunction and $p$ $x$ can be assumed while checking $p'$ $x$. The well-formedness of the right-hand side (RHS) follows. Verifying the equality is straightforward by showing subtyping in both directions. (QQ): well-formedness of the LHS yields $r:A \rightarrow A \rightarrow \mathbf{bool}$ and $r':A/r \rightarrow A/r \rightarrow \mathbf{bool}$, so $A \prec: A/r$ implies $r'$ $x$ $y$ (and thus the RHS) is well-formed. The relation on the RHS is an equivalence relation since $r'$ is. To verify the type equality, we use Lemma 2 and show that both types induce the same equality. In particular, the type of $r'$ already guarantees that it subsumes $r$.

(RQ): well-formedness of the LHS yields $r:A \rightarrow A \rightarrow \mathbf{bool}$ and $p:A/r \rightarrow \mathbf{bool}$, implying $r:A|_p \rightarrow A|_p \rightarrow \mathbf{bool}$ and $p:A \rightarrow \mathbf{bool}$. The well-formedness of the RHS follows. (Note the other direction does not hold in general.) To show the equality, we show both subtyping directions. For LHS $\prec$:RHS, we assume $x:A/r$ and $p$ $x$ and apply the elimination rule for quotients using $t=x$ and $B=(A|_p)/r$. (Critically, this step would not go through if we had only used the weaker rule $*$ in Sect. 5.) For RHS $\prec$:LHS, we assume $x:(A|_p)/r$ and apply the elimination rule for quotients using $t=x$.

**Theorem 6 (Refinement/Quotient in a Function Type).** The following are derivable if either side is well-formed:

$$ \vdash_T \Pi x: A. (B|_p) \equiv (\Pi x: A. B)|_{\lambda f: (\Pi x: A. B)}. \forall x: A. p (f x) \qquad (RCod) $$

$$ \vdash_T \Pi x:A/r. B \equiv (\Pi x:A. B)|_{\lambda f: \Pi x:A. B. \forall x,y:A. r x y \Rightarrow (f x) =_B (f y)} \qquad (QDom) $$

$$ \vdash_T \Pi x:A. B/r :\succ (\Pi x:A. B)/\lambda f, g:\Pi x:A. B. \forall x:A. r (f x) (g x) \qquad (QCod) $$

The following is derivable if the RHS is well-formed:

$$ \vdash_T \Pi x:A|_p . B :\succ (\Pi x:A.B)/\lambda f, g:\Pi x:A.B. \forall x:A. p x \Rightarrow (f x) =_B (g x) \qquad (RDom) $$

**Proof. (RCod):** Both subtyping directions are straightforward, as terms on either side are given by $\lambda x:A. t$ where $t$ has type $B$ and satisfies $p$.

(QDom): Both subtyping directions are straightforward, as both sides are subtypes of $\Pi x:A. B$ so their elements must preserve $r$.

(RCod): Assume a term $f$ of RHS-type and show $x:A \vdash f x:B/r$ using the rules for quotients.

(RDom): Assume a term $f$ of RHS-type and show $x:A|_p \vdash f x:B$ using the quotient elimination rule. The well-formedness of the LHS does not imply the well-formedness of the RHS since the well-formedness of $B$ can rely on $p$ $x$.

Maybe surprisingly, two of the subtyping laws in Theorem 6 are not equalities. The law for the refined domain must not be an equality:

**Example 5 (Refined Domain (RDom)).** The assumption $p$ $x$ makes more terms well-typed, thus there may be functions $\Pi x:A|_p$. $B$ that are not a restriction of a function $\Pi x:A. B$. Consider the theory $a:\mathbf{bool} \rightarrow tp, c:\mathbf{true}$. Then a false is empty and so are $\Pi x:\mathbf{bool}. a x$ and its quotients. But with $p = \lambda x:\mathbf{bool}. x$, we have $\vdash \lambda x:\mathbf{bool}|_p . c : \Pi x:\mathbf{bool}|_p . a x$.
The law for the quotiented codomain may or may not be an equality. This is related to the axiom of choice. Consider the two statements

$$ \vdash_T \exists repr:B/r \rightarrow B. \quad repr =_{B/r \rightarrow B/r} \lambda x:B/r. x \\ f:\Pi x:A. B/r \vdash_T \exists g:\Pi x:A. B. \quad f =_{\Pi x:A. B/r} g $$

(Note that the first one is well-typed because $B \prec: B/r$.) Both have a claim to be called the axiom of choice: The first one expresses that every equivalence relation has a system of representatives. The second generalizes this to a family of equivalence relations. The latter implies the former (put $A := B/r$ and $f := \lambda x:B/r. x$). In the simply-typed case the former also implies the latter (pick $repr \circ f$ for $g$); but in the dependently-typed case, $B$ and $r$ may depend on $x$ and the implication might not hold.

Both statements construct a new term from an existing one (*repr* behaves like the identity, and *g* like *f*) that has a different type but behaves the same up to quotienting. If the direction $\prec$: were to hold in the law for the refined codomain, it would not only imply the existence of *g* from *f* but also allow using *f* as a representative of the equivalence class of possible values for *g*. That is in keeping with our goal of avoiding changes of representation. Therefore:

**Definition 2 (Quotiented Codomain).** We adopt the rule below (which is an equality with Theorem 6) as an axiom whenever either side is well-formed:

$$ \vdash_T \Pi x:A. B/r \prec: (\Pi x:A. B)/\lambda f, g:\Pi x:A. B. \forall x:A. r (f x) (g x) \quad (**) $$

Aggregating the above laws, we obtain a normalization algorithm for types:

**Theorem 7 (Normalizing Types).** Every type is equal to a type of the form $(A|_p)/r$ where $A, B ::= \mathbf{bool} \mid a^* \mid \Pi x:A|_p$. $B$. In particular, if a type does not use refined domains, it is equal to a quotient of a refinement of a DHOL type.

*Proof.* Using Theorem 6 with the axiom from Definition 2, all refinements and quotients can be pushed out of all function types except for a single refinement of the domain; if there is no such refinement, we can use $p := \lambda x:A. true$. And using Theorem 5, those can be collected into a single quotient+refinement.

Together with the equality and variance rules from Theorems 2, 3, 4, this induces a **subtype-checking algorithm** that reduces subtyping to validity without ever expanding Definition 1. The latter is important because expanding Definition 1 would recurse into a computationally expensive problem. This algorithm is obviously sound as it only chains derived rules. We are confident, but have not proved yet, that it is also complete in the sense that subtyping can always be derived by using only our derived rules (i.e., without Definition 1) and a sound and complete theorem prover (which we obtain in Sect. 7).

It may be surprising and certainly complicates subtype-checking that we need to allow for refined domains in the normal forms. This limitation echoes an
observation first made in [14] about combining dependent types and refinements. Effectively, the culprits are partial dependent functions that cannot be extended to total functions because the return type is well-defined and non-empty only for the refined domain. For future work, it would be interesting to use a higher-order logic with partial functions as a translation target, like the one of [10]. But we have not considered that option due to the lack of ATP support for such logics.

# 7 Soundness and Completeness

We extend the translation from Fig. 3 with cases for our two new productions:

$$ \overline{A|_p} := \overline{A} \qquad (A|_p)^* s t := A^* s t \wedge \overline{p} s \wedge \overline{p} t $$

$$ \overline{A/r} := \overline{A} \qquad (A/r)^* s t := \overline{r} s t \wedge A^* s s \wedge A^* t t $$

These definitions are not surprising as PERs in HOL are known to be closed under refinements and quotients.

**Example 6 (PERs for a Quotiented Codomain).** We calculate the PERs for both sides of the law for quotiented codomains in Theorem 6:

$$ (\Pi x: A. \overline{B/r})^* f g \\ = \forall x, y: \overline{A}. A^* x y \Rightarrow (\overline{r} (f x) (g y) \wedge B^* (f x) (f x) \wedge B^* (g y) (g y)) $$

Both this and $((\Pi x: A. B)/\lambda f, g:\Pi x: A. B. \forall x: A. r (f x) (g x))^* f g$ simplify to $\forall x: \overline{A}. A^* x x \Rightarrow \overline{r} (f x) (g x) \wedge B^* (f x) (f x) \wedge B^* (g x) (g x)$. This justifies adopting axiom (**) . The simplification uses the substitution lemma from the extended preprint [5], the well-definedness of $r$, and the transitivity of $\overline{r}$.

**Example 7 (PERs for a Refined Domain).** We calculate the PERs for both sides of the law for refined domains in Theorem 6:

$$ (\Pi x: A|_p. B)^* f g = \forall x, y: \overline{A}. A^* x y \wedge \overline{p} x \wedge \overline{p} y \Rightarrow B^* (f x) (g y) $$

$$ ((\Pi x: A. B)/\lambda f, g:\Pi x: A. B. \forall x: A. p x \Rightarrow (f x) =_B (g x))^* f g = \\ \forall x: \overline{A}. (A^* x x \Rightarrow \overline{p} x \Rightarrow B^* (f x) (g x)) \wedge \\ (\forall x, y: \overline{A}. A^* x y \Rightarrow B^* (f x) (f y)) \wedge \\ (\forall x, y: \overline{A}. A^* x y \Rightarrow B^* (g x) (g y)) $$

These are indeed not equivalent in line with our observation from Example 5.

Like in [22], this translation yields a sound (defined as in the previous paper) and complete theorem prover:

**Theorem 8 (Completeness).** We have the invariants from Fig. 4.

*Proof.* The subtyping claim is a slightly strengthened version of the claim obtained by expanding the definition of $<:$. The proof, given in the extended preprint [5], adapts the proof from [22] with additional cases for new productions and rules.
<table><caption>**Fig. 4.** Invariants of the Translation</caption><thead><tr><th>if in DHOL</th><th>then in HOL</th></tr></thead><tbody><tr><td>Γ ⊢ T Thy</td><td>Γ ⊢ T Thy</td></tr><tr><td>Γ ⊢ T Γ Ctx</td><td>Γ ⊢ T Γ Ctx</td></tr><tr><td>Γ ⊢ T A tp</td><td>Γ ⊢ T A tp and Γ ⊢ T A* : A → A → bool and A* is a PER</td></tr><tr><td>Γ ⊢ T A ≡ B</td><td>Γ ⊢ T A ≡ B and Γ, x, y : A ⊢ T A* x y = bool B* x y</td></tr><tr><td>Γ ⊢ T A ≺ : B</td><td>Γ ⊢ T A ≡ B and Γ, x, y : B ⊢ T A* x y ⇒ B* x y</td></tr><tr><td>Γ ⊢ T t : A</td><td>Γ ⊢ T t : A and Γ ⊢ T A* t t</td></tr><tr><td>Γ ⊢ T F</td><td>Γ ⊢ T F</td></tr></tbody></table>

As in [22], the converse of Theorem 8 is much harder to state and prove. First we need a technical assumption: We call a type symbol a *inhabited* if at least one of its instances is provably non-empty.

**Theorem 9 (Soundness).** In a well-formed DHOL-theory $Γ ⊢ T Thy$ in which every type symbol is inhabited:

If $Γ ⊢_{T}^{DHOL} F : bool$ and $Γ ⊢_{T}^{HOL} F$, then $Γ ⊢_{T}^{DHOL} F$

*Proof.* The key idea is to transform a HOL-proof of $F$ into one that is in the image of the translation, at which point we can read off a DHOL-proof of $F$. The full proof is given in the extended preprint [5]. We expect the inhabitation requirement to be redundant, but have not been able to complete the proof without it yet. In any case, it is harmless because it is satisfied by all practical examples.

It is now straightforward to extend the DHOL implementation we gave in [22]: First run a bidirectional type-checker for DHOL, using the subtyping-checker sketched in Sect. 6, to establish well-typedness of theory and conjecture. Then translate conjecture and generated proof obligations and apply a HOL ATP.

# 8 Application to Typed Set Theory

DHOL with subtyping enables a novel formalization of typed set-theory:

set: tp, ∈ : set → set → bool, elem s := set|λx: set. x ∈ s

The key idea is that *elem s* is the DHOL *type* of set-theoretical elements of the *set s*. Leveraging that refinements and quotients do not require change of representation, we obtain a powerful combination of elegant high-level typed formalization and efficient low-level reasoning. All the routine constructions of untyped set theory can be lifted to their typed counterparts. For example, for products, we use $×: set → set → set$ and *pair: set → set → set* and the property
▷ ∀ x, y, s, t : set. ( x ∈ s ) ∧ ( y ∈ t ) ⇒ pair x y ∈ s × t , from which we can show that pair : elem s → elem t → elem ( s × t ) .

We can also use DHOL-functions set → set as set-theoretical func-
tions between sets s and t without a change in representation as the type
Functions st := (set → set)|_p/r where p f = ∀ x : set. x ∈ s ⇒ (f x ) ∈ t and
r f g = ∀ x : set. x ∈ s ⇒ (f x ) =_set (g x ). This allows us to represent set-
theoretical function application and composition ◦ directly as DHOL applica-
tion/composition.

Consequently, theorem proving in typed set theory becomes very strong
because a large share of the proving workload can be outsourced into typing-
obligations. For example, the property that the composition of functions f :
Functions s t and g : Functions t u has type Functions s u becomes

$$
\vdash \forall s, t, u : \text{set.} \quad \forall f : \text{Functions s t.} \quad \forall g : \text{Functions t u.} \quad \forall x : \text{set.} \quad x \in s \Rightarrow ((g \circ f) x) \in u
$$

which yields in HOL the conjecture below that current HOL ATPs solve easily.

$$
\triangleright \forall s:\mathit{set\_rel} s s \Rightarrow \forall t:\mathit{set\_rel} t t \Rightarrow \forall u:\mathit{set\_rel} u u \Rightarrow
$$

$$
\forall f:\mathit{set} \to \mathit{set}. \forall x:\mathit{set}. x \in s \Rightarrow \mathit{set\_rel}(f x)(f x) \wedge (\forall x:\mathit{set}. x \in s \Rightarrow (f x) \in t) \Rightarrow
$$

$$
\forall g:\text{set} \to \text{set}. \forall x:\text{set}. x \in t \Rightarrow \text{set\_rel}(g x)(g x) \wedge (\forall x:\text{set}. x \in t \Rightarrow (g x) \in u) \Rightarrow
$$

$$
\forall x:\mathit{set\_rel} u \Rightarrow x \in s \Rightarrow ((g(fx)) \in u)
$$

Below is the HOL translation of the conjecture that function composition is
associative. It is similarly easily proved by current ATPs:

$$
\triangleright \forall s:\mathit{set\_rel} s s \Rightarrow \forall t:\mathit{set\_rel} t t \Rightarrow \forall u:\mathit{set\_rel} u u \Rightarrow \forall v:\mathit{set\_rel} v v \Rightarrow
$$

$$
\forall f:\mathit{set} \to \mathit{set}. \forall x:\mathit{set}. x \in s \Rightarrow \mathit{set\_rel}(f x)(f x) \wedge (\forall x:\mathit{set}. x \in s \Rightarrow (f x) \in t) \Rightarrow
$$

$$
\forall g:\mathit{set} \to \mathit{set}. \forall x:\mathit{set}. x \in t \Rightarrow \mathit{set\_rel}(g x)(g x) \wedge (\forall x:\mathit{set}. x \in t \Rightarrow (g x) \in u) \Rightarrow
$$

$$
\forall h:\mathit{set} \to \mathit{set}. \forall x:\mathit{set}. x \in u \Rightarrow \mathit{set\_rel}(h x)(h x) \wedge (\forall x:\mathit{set}. x \in t \Rightarrow (h x) \in v) \Rightarrow
$$

$$
\forall x:\mathit{set}. \mathit{set\_rel} x x \Rightarrow x \in s \Rightarrow (\mathit{set\_rel} (h (g (f x))) (h (g (f x))))
$$

The corresponding TPTP files are available at https://gl.mathhub.info/MMT/LATIN2/-/tree/master/source/casestudies/2025-FroCos.

9 Conclusion and Future Work

DHOL combines higher-order logic with dependent types, obtaining an intuitive
and expressive language, albeit with undecidable typing. We double down on
this design by elegantly extending DHOL with two practically important type
constructors that thrive in that setting: refinement and quotient types. Like
dependent function types, these two require terms occurring in types. Both are
near-impossible to add as an afterthought to a type theory with decidable typing.

We translate the resulting logic to HOL, obtaining a practical automated
theorem proving workflow for DHOL with refinement and quotient types. Our
main result is the proof of soundness and completeness of this translation.
We used an extensional subtyping approach, where *A*<:*B* holds iff all *A*-terms also have type *B*. This allows combining typed representations and efficient reasoning. We established all the expected variance and normalization laws except for function types with refined domains. Future work must investigate how to improve on this to make normalizing types and thus subtype-checking simpler.

We also want to carry our results for DHOL over to existing refinement/quotient type systems for programming languages like Quotient Haskell, where DHOL-like axioms are used as lightweight specifications.

## References

1. Allen, S.: A non-type-theoretic semantics for type-theoretic language. Ph.D. thesis, Cornell University (1987)

2. Andrews, P.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press (1986)

3. Hewer, B., Hutton, G.: Quotient Haskell: lightweight quotient types for all. Proc. ACM Program. Lang. 8(POPL) (2024). https://doi.org/10.1145/3632869

4. Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261–279. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_17

5. Rothgang, C., Rabe, F.: Subtyping in DHOL – Extended preprint (2025). https://arxiv.org/abs/2507.02855

6. Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(1), 56–68 (1940)

7. Constable, R., et al.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall (1986)

8. Coq Development Team: The Coq Proof Assistant: Reference Manual. Technical report, INRIA (2015)

9. de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26

10. Farmer, W.: A simple type theory with partial functions and subtypes. Ann. Pure Appl. Logic 64(3), 211–240 (1993)

11. Gordon, M.: HOL: a proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P. (eds.) VLSI Specification, Verification and Synthesis, pp. 73–128. Kluwer-Academic Publishers (1988)

12. Homeier, P.V.: A design structure for higher order quotients. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 130–146. Springer, Heidelberg (2005). https://doi.org/10.1007/11541868_9

13. Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03545-1_9

14. Hurd, J.: Predicate subtyping with predicate sets. In: Boulton, R., Jackson, P. (eds.) Theorem Proving in Higher Order Logics, pp. 265–280 (2001)

15. Kunčar, O., Popescu, A.: Comprehending Isabelle/HOL’s consistency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 724–749. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_27
16. Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Proceedings of the 1973 Logic Colloquium, pp. 73–118. North-Holland (1974)

17. Niederhauser, J., Brown, C., Kaliszyk, C.: Tableaux for automated reasoning in dependently-typed higher-order logic. In: Benzmüller, C., Heule, M., Schmidt, R. (eds.) Automated Reasoning, pp. 86–104. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-63498-7_6

18. Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217

19. Popescu, A., Traytel, D.: Admissible types-to-pers relativization in higher-order logic. Proc. ACM Program. Lang. 7 (POPL) (2023). https://doi.org/10.1145/3571235

20. Ranalter, D., Brown, C., Kaliszyk, C.: Experiments with choice in dependently-typed higher-order logic. In: Bjørner, N., Heule, M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence and Reasoning, pp. 311–320 (2024)

21. Ranalter, D., Rabe, F., Kaliszyk, C.: Polymorphic theorem proving for DHOL

22. Rothgang, C., Rabe, F., Benzmüller, C.: Theorem proving in dependently typed higher-order logic. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction, pp. 438–455. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-38499-8_25

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
# Satisfiability Modulo Theories
# Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories

Gabriele Masina(✉) and Roberto Sebastiani(✉)

DISI, University of Trento, Trento, Italy
{gabriele.masina,roberto.sebastiani}@unitn.it

**Abstract.** Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) with the task of optimizing some objective function(s). In OMT solvers, a CDCL-based SMT solver enumerates theory-satisfiable total truth assignments, and a theory-specific procedure finds an optimum model for each of them; the current optimum is then used to tighten the search space for the next assignments, until no better solution is found.

In this paper, we analyze the role of truth-assignment enumeration in OMT. First, we spotlight that the enumeration of *total* truth assignments is suboptimal, since they may over-restrict the search space for the optimization procedure, whereas using *partial* truth assignments instead can improve the effectiveness of the optimization. Second, we propose some assignment-reduction techniques for exploiting *partial-assignment enumeration* within the OMT context. We implemented these techniques in the OPTIMATHSAT solver, and we conducted an experimental evaluation on OMT benchmarks. The results confirm the improvement in both the efficiency of optimal solving and the quality of the obtained solutions for anytime solving.

**Keywords:** Optimization Modulo Theories · Enumeration · Partial Assignments

## 1 Introduction

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a logical formula w.r.t. some background theory, such as linear and nonlinear arithmetic, bit-vectors, arrays, or uninterpreted functions [2]. Many SMT-encodable problems also require the capability of finding models that are optimal w.r.t. some objective functions. These problems are grouped under the term Optimization Modulo Theories (OMT) [6,25,31]. OMT has been successfully applied to a wide range of problems, such as verification of timed and hybrid systems [14,31], numeric [16] and temporal planning [26,27], optimal scheduling [7], constrained goal modelling [24], hybrid machine learning [37], GAS optimization for smart contracts [1], and optimum encodings for quantum annealing [3,10], establishing OMT solvers as powerful tools for solving complex constraint optimization problems in various domains.

**OMT Solving.** A general OMT-solving strategy [25,31,32] consists in performing a sequence of incremental SMT calls, progressively tightening the range of values for the
objective function. Specifically, an SMT solver is used to enumerate *T*-satisfiable truth assignments that propositionally satisfy the problem formula $\varphi$. For each such truth assignment, a *T*-optimizer finds a *T*-model of optimum cost within it. A constraint is then added to the formula to tighten the upper bound for the cost of the optimum model, and the search continues until the formula is found unsatisfiable. Besides optimal solving, an important feature of OMT solvers is the ability to provide the user with a good-enough solution within a given time budget. This capability, known as *anytime* OMT solving, is especially valuable in industrial applications where finding the optimum solution may be computationally impractical, and it is rather more important to obtain high-quality solutions quickly.

OMT techniques have been developed for *LRA* [6,32], *LIRA* [6,33], *NRA* [4], *NIA* [4], *BV* [23,39], and *FP* [39]. Also, OMT has been extended to deal with multiple objectives including lexicographic OMT [6,33], boxed OMT [6,17,33], min-max OMT [34], and Pareto OMT [6]. Recently, a Generalized OMT calculus has been proposed, extending the definition to objectives over partially ordered sets [41].

*Partial Assignments Enumeration in SMT.* The problem of truth assignment enumeration has been studied in recent years, mainly in the context of SAT and SMT enumeration (AllSAT and AllSMT). Typically, enumeration algorithms [12, 13, 15, 35, 36] rely their efficiency on the enumeration of partial assignments to reduce both the number of enumerated assignments and the computational time by up to an exponential factor. Several techniques have been proposed to find short satisfying partial assignments starting from a total assignment, trading off efficiency for effectiveness (e.g., [22, 29, 38]). Also, the impact of CNF-ization on the effectiveness of partial assignment reduction has been recently studied in [20,21].

*Contributions.* In this paper, we study the applicability of enumeration-based techniques to OMT solving, and, in particular, the usage of partial truth assignment reduction to improve the effectiveness and efficiency of OMT solving. First, we notice that OMT solvers typically invoke the *T*-optimizer on total truth assignments, and we spotlight how this can be suboptimal in many cases. Second, we propose some ways to exploit partial truth assignments in OMT solving, tailoring existing techniques to the OMT context. We discuss the general idea for an arbitrary theory, and describe an implementation for the specific case of linear arithmetic over *LRA* and *LIRA*, possibly combined with other theories. We implemented these strategies in the OMT solver OPTIMATHSAT [34], and we show through an empirical evaluation over OMT(*LRA*), OMT(*LIRA*), and OMT(*LRA* ∪ *AR*) benchmarks that they improve both the efficiency of optimal solving and the quality of obtained solutions for anytime solving.

*Related Work.* The idea of using partial assignments in OMT(*LIRA*) has been previously considered in [5, 18]. In [5], the authors mention that in lazy OMT-solving, the truth assignments should preferably be prime implicants. This approach, however, is theory-blind; our reduction techniques, instead, specifically target theory-literals involved in optimization, which proves crucial for the solver efficiency. A similar idea was proposed in [18], where the truth assignments are reduced to prime implicants before invoking the *T*-solver and *T*-minimizer. Though our work is similar in flavour
to theirs, there are some key differences: (a) their enumeration algorithm only adds clauses blocking the minimized truth assignment, whereas modern OMT solvers add cost bounds (cost < ub) to prune the search space, which has been shown to be much more effective; (b) we also propose a cost-guided technique, which we show to perform much better in practice.

*Organization.* The rest of the paper is organized as follows. In Sect. 2, we provide the necessary background on SMT and OMT solving. In Sect. 3, we analyze the role of total and partial truth assignments in OMT solving. In Sect. 4, we propose two strategies to exploit partial truth assignments in OMT solving. In Sect. 5, we present an experimental evaluation of the proposed strategies over OMT(LRA), OMT(LIRA), and OMT(LRA∪AR) benchmarks. Finally, in Sect. 6, we conclude the paper and discuss future work.

## 2 Background

*Notation and Terminology.* We assume the standard setting with quantifier-free first-order formulas, and the standard notions of theory, satisfiability, logical consequence. We assume the reader is familiar with these notions and with the lazy CDCL-based SMT-solving approach, and refer to [2] for a comprehensive introduction to SMT.

In this paper, we denote SMT formulas by $\varphi$, theories by $\mathcal{T}$, variables by $x, y$, atoms by $\alpha$, truth assignments by $\mu, \eta$, and models by $\mathcal{M}$; all symbols possibly with subscripts or superscripts. We denote by $\mathit{Atoms}(\varphi)$ the set of atoms occurring in a formula $\varphi$.

### 2.1 Satisfiability Modulo Theories

Given a first-order theory $\mathcal{T}$, a $\mathcal{T}$-atom is any atomic formula built over the signature of $\mathcal{T}$. A $\mathcal{T}$-literal is a $\mathcal{T}$-atom or its negation. A $\mathcal{T}$-formula is either a $\mathcal{T}$-literal or a combination of formulas by means of standard Boolean operators. From now on, we assume every formula is in Conjunctive Normal Form (CNF), i.e., it is a conjunction ($\wedge$) of clauses, where each clause is a disjunction ($\vee$) of literals. (If it is not, then it can be easily converted into CNF by applying the standard transformations [28,40]).

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula w.r.t some first-order theory $\mathcal{T}$, or combination of first-order theories $\mathcal{T} \cup \mathcal{T}'$. A formula is $\mathcal{T}$-satisfiable if it is satisfiable in a model of $\mathcal{T}$ (a $\mathcal{T}$-model). Popular theories include linear and nonlinear arithmetic over the reals or integers $(\mathcal{LRA}, \mathcal{NRA}, \mathcal{LIRA}, \text{and } \mathcal{NIRA})$, bit-vectors $(\mathit{BV})$, and floating-point $(\mathit{FP})$.

*Lazy SMT-Solving.* Given a formula $\varphi$ with $\mathit{Atoms}(\varphi) = \{\alpha_1, \dots, \alpha_n\}$, a truth assignment $\mu : \mathit{Atoms}(\varphi) \to \{\top, \bot\}$ maps atoms in $\varphi$ to truth values. A partial truth assignment is a partial mapping, and a total truth assignment is a total mapping. We represent a truth assignment $\mu$ also as a conjunction of literals $\bigwedge_{\mu(\alpha_i)=\top} \alpha_i \wedge \bigwedge_{\mu(\alpha_i)=\bot} \neg \alpha_i$. We say that $\mu$ propositionally satisfies $\varphi$ iff $\mu$ satisfies all clauses in $\varphi$.

The CDCL($\mathcal{T}$) algorithm [19] is based on the so-called lazy approach to SMT (see e.g., [2,30]), which exploits the fact that a $\mathcal{T}$-formula $\varphi$ is $\mathcal{T}$-satisfiable iff there exists
a truth assignment $\mu$ that propositionally satisfies $\varphi$ and $\mu$ is $\mathcal{T}$-satisfiable. It combines a CDCL-based SAT-solver with a $\mathcal{T}$-specialized decision procedure called $\mathcal{T}$-solver to decide the consistency of a set of $\mathcal{T}$-literals. Whenever the SAT-solver finds a truth assignment $\mu$ propositionally satisfying $\varphi$, it invokes the $\mathcal{T}$-solver to check the $\mathcal{T}$-satisfiability of $\mu$. If $\mu$ is $\mathcal{T}$-satisfiable, then the $\mathcal{T}$-solver returns a model $M$, that is also a model of $\varphi$. Otherwise, the $\mathcal{T}$-solver returns a subset of $\mu$ that causes the $\mathcal{T}$-unsatisfiability, which is learned by the SAT-solver and used in subsequent iterations to prune the search space.

To maximize efficiency, most $\mathcal{T}$-solvers can be called incrementally via a stack-based interface, keeping the status of the search between calls. E.g., an efficient, incremental $\mathcal{LRA}$-solver, can be built on a variant of the Simplex algorithm designed to be integrated within a lazy SMT framework [11]. The combination of theories can be handled efficiently by delayed theory combination [8].

Another important feature of CDCL-based SMT solvers is that they provide a stack-based incremental interface, allowing to push and pop clauses and incrementally check the satisfiability of the formula conjoined with the pushed clauses, maintaining most of the learned information between calls.

## 2.2 Optimization Modulo Theories

Let $\mathcal{T}$ be a theory admitting some total order relation “$\le$” over its domain, let $\varphi$ be a $\mathcal{T}$-formula, and let cost be a $\mathcal{T}$-term which we call objective function. Optimization Modulo Theories (OMT($\mathcal{T}$)) is the problem of finding a model for $\varphi$ that makes the value of cost minimum according to the order given by $\le$ (maximization is dual) [4, 31]. To simplify the presentation, we focus on minimization, but the same concepts apply to maximization as well. Notice that, in general, $\varphi$ can be built on a combination of $\mathcal{T}$ with other theories (OMT($\mathcal{T} \cup \mathcal{T}'$)), and the same concepts apply to such cases [31, 32].

*Example 1.* Consider the $\mathcal{LRA}$-formula on the rational variables $x, y$:

$$ \varphi \stackrel{\text{def}}{=} \left( \begin{array}{l} ((2x - 3y \le 6) \lor (x \le 4)) \land \\ ((y \le 2) \lor (y \le -3x + 9) \lor (x < -2)). \end{array} \right) \tag{1} $$

$\varphi$ is $\mathcal{LRA}$-satisfiable, e.g., the $\mathcal{LRA}$-model $M \stackrel{\text{def}}{=} \{x \mapsto 3, y \mapsto 0\}$ satisfies $\varphi$.

Consider the OMT($\mathcal{LRA}$) problem $\langle\varphi, \text{cost}\rangle$ where $\varphi$ is the $\mathcal{LRA}$-formula in (1), and cost $\stackrel{\text{def}}{=} -2x$. Then the model $M \stackrel{\text{def}}{=} \{x \mapsto 3, y \mapsto 0\}$ has cost $= -6$. A better model of $\varphi$ is, e.g., $M' \stackrel{\text{def}}{=} \{x \mapsto 6, y \mapsto 2\}$, that has cost $= -12$. This model is also the model of $\varphi$ with minimum cost.

*Lazy OMT Solving.* A general optimization strategy implemented by state-of-the-art OMT solvers, and typically used for OMT($\mathcal{LRA}$) and OMT($\mathcal{LIRA}$), is the so-called linear-search strategy [25, 31, 32]. It consists in solving a sequence of SMT problems where the space of feasible solutions is progressively tightened by learning unit clauses in the form (cost < ub), ub being the currently-known upper bound for cost. At each iteration, the solver can either find a model $M$ whose value of cost is smaller than ub, or detect the unsatisfiability of the current formula. In the first case, the solver invokes
a *T*-specific procedure, called *T*-minimizer, to find an optimum model $M'$ within the
truth assignment induced by *M*. Then, ub is set to $M'(\text{cost})$, and the search continues.
In the second case, the formula has no models with cost lower than ub, and the search
terminates as the last model found is optimum.

Alternatively, the solver could also follow a *binary-search* strategy [31]. In this case, a lower and upper bound lb and ub are kept s.t. the optimum model lies in the interval (lb, ub]. At each iteration, an intermediate value pivot $\in$ (lb, ub] is chosen, and the solver checks if there exists a model with cost lower than pivot. If so, pivot becomes the new upper bound, otherwise, it becomes the new lower bound. The search terminates when lb and ub are equal, and the last model found is optimum. (In continuous domains, e.g., OMT($LRA$), to guarantee termination, it is necessary to interleave binary-search steps with a linear-search step [31]). In this paper, we focus on the linear-search strategy, but the analysis applies to the binary-search strategy as well.

If $\varphi$ is built on a combination of theories, then the *T*-minimizer is invoked on $\mu_T \cup \mu_{ed}$—i.e., the subset of $\mu$ containing only the atoms in *T* and the interface (dis-)equalities [31,32] The implementation of *T*-minimizers for *LRA* and *LIRA* is briefly described in the next paragraph.

*T*-minimizers. A *LRA*-minimizer [31,32] can be implemented as a simple extension of the Simplex-based *LRA*-solver [11]. For *LIRA*, a minimizer can be built on top of a branch-and-bound *LIRA*-solver [5,6,33], by replacing the *LRA*-solver with a *LRA*-solver&minimizer to solve each relaxed subproblem. To find an optimum model within the truth assignment, once a *LIRA*-model *M* is found, a constraint (cost < $M(\text{cost})$) is pushed onto the *LIRA*-solver, and the search is iteratively refined until no better model exists. An alternative strategy, implemented, e.g., in OPTIMATHSAT, is the so-called *truncated* optimization [33], where the *LIRA*-minimizer stops after finding the first model *M*. Although this model may be sub-optimal for the current truth assignment—allowing the same assignment to be found again by the CDCL(*T*) procedure—this approach is typically much faster and remains effective in practice.

*Remark 1.* Importantly, the lazy OMT solving approach allows for an *anytime* behavior, i.e., we can interrupt the search at any time and return the best model found so far.

## 2.3 SAT and SMT Enumeration

SAT enumeration (AllSAT) is the problem of finding all the truth assignments that propositionally satisfy a propositional formula. SMT enumeration (AllSMT) is the problem of finding all *T*-satisfiable truth assignments that propositionally satisfy a *T*-formula. Since a partial assignment can be extended to $2^k$ total truth assignments, $k$ being the number of unassigned atoms, finding short partial truth assignments is a key point in reducing both the number of enumerated truth assignments and the computational time by up to an exponential factor.

Many enumeration algorithms find total truth assignments, and then extract partial
truth assignments from them by some reduction procedure. A basic reduction proce-
dure is illustrated in Algorithm 1. It consists in iteratively dropping literals one-by-one
from the truth assignment, checking if it still satisfies the formula. The resulting partial
**Algorithm 1. REDUCE-ASSIGNMENT($\varphi$, $\eta$)**

**Input:** CNF formula $\varphi$, $\mathcal{T}$-satisfiable total truth assignment $\eta$ satisfying $\varphi$

**Output:** Reduced (minimal) partial truth assignment $\mu \subseteq \eta$ satisfying $\varphi$

1: $\mu \leftarrow \eta$

2: **for** $\ell \in \mu$ **do**

3: &nbsp;&nbsp;&nbsp;&nbsp;**if** $\mu \setminus \{\ell\}$ satisfies all clauses in $\varphi$ **then**

4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**$\mu \leftarrow \mu \setminus \{\ell\}$**

5: **return** $\mu$

assignment is minimal, i.e., it cannot be further reduced without violating the satisfaction of the formula. Notice that the order in which literals are dropped can have a significant impact on the effectiveness of the reduction procedure.

## 3 An Analysis of Enumeration in OMT

In the following, to simplify the notation and the presentation, we refer to one single theory $\mathcal{T}$, but the results can be straightforwardly extended to combinations of theories.

As described in Sect. 2.2, a basic OMT solving schema involves the interaction of a combinatorial and a theory-specific optimization components. In the combinatorial component, an SMT solver enumerates $\mathcal{T}$-satisfiable truth assignments that propositionally satisfy the problem formula $\varphi$ conjoined with increasingly tighter bounds on the cost of the optimum solution. In the theory-specific component, a $\mathcal{T}$-minimizer finds a $\mathcal{T}$-model of minimum cost within the constraints imposed by the given truth assignment. This model is then used to tighten the upper bound for the cost of the optimum model and continue the search, until the formula is found unsatisfiable.

Since the enumeration is based on the CDCL($\mathcal{T}$) schema [19], these truth assignments are typically *total*, i.e., they assign a truth value to each atom of the formula. However, we point out that total truth assignments can often over-constrain the search space for the optimum model, whereas relying on *partial* truth assignments can be much more effective. Intuitively, *by removing from the current satisfying truth assignment* $\mathcal{T}$-constraints that are not strictly necessary for the propositional satisfaction of the formula, we enlarge the area within which the optimum model is searched, thus increasing the chances of finding a better optimum model. This means that the solver can add a tighter upper bound to the cost of the global optimum, potentially reducing the number of search iterations needed to find it, and consequently the overall solving time. Moreover, this improvement can be crucial for anytime OMT solving, as it allows the solver to converge faster to better solutions within the given time limit.

We illustrate this idea in the following example.

**Example 2.** Consider the OMT($\mathcal{LRA}$) problem $\langle\varphi, \text{cost}\rangle$ where $\varphi$ is the formula in (1) in Example 1, and cost $\stackrel{\text{def}}{=} -2x$. Consider the following scenario, which is graphically represented in Fig. 1. Consider the $\mathcal{LRA}$-satisfiable total truth assignment that propositionally satisfies $\varphi$:

$$ \mu \stackrel{\text{def}}{=} \{(2x - 3y \le 6), (y \le 2), \neg(x < -2), (y \le -3x + 9), (x \le 4)\}. \quad (2) $$
<figure><img src="image_27.png" /><figcaption>**Fig. 1.** Graphical representation of Example 2. For each step, the half-planes representing the constraints in the truth assignment are delimited by dashed lines and colored in grey. The intersection of these constraints is colored in blue, with a gradient that follows the value of cost (the lower the value of cost, the more intense the color), and the red dot represents the optimum model found within this region. (Color figure online)</figcaption></figure>

The optimum model of $\mu$ is $\{x \mapsto 3, y \mapsto 0\}$ with cost $= -6$ (Fig. 1a). We notice that some literals in $\mu$ are not strictly necessary for propositionally satisfying $\varphi$. In fact, we only need one true literal in each clause to propositionally satisfying the formula. Not every drop is equally effective, though. For instance, if we drop $(x \le 4)$, $(y \le 2)$, or $\neg(x < 2)$, then we get a truth assignment with the same optimum as $\mu$, since these literals don't "oppose" to the optimization of cost in $\mu$. Dropping at least one of the other two literals, instead, leads to a truth assignment with a better optimum model. For instance, if we drop $(y \le -3x + 9)$, we get:

$$ \mu' \stackrel{\text{def}}{=} \mu \setminus \{(y \le -3x + 9)\} = \{(2x - 3y \le 6), (y \le 2), \neg(x < -2), (x \le 4)\}. \quad (3) $$

The optimum model of $\mu'$ is $\{x \mapsto 4, y \mapsto 2/3\}$ with cost $= -8$ (Fig. 1b). At this point, two constraints, $(x \le 4)$ and $(2x - 3y \le 6)$, oppose to the optimization of cost, and either of them can be safely dropped. Assume that we drop $(x \le 4)$, then we get:

$$ \mu'' \stackrel{\text{def}}{=} \mu' \setminus \{(x \le 4)\} = \{(2x - 3y \le 6), (y \le 2), \neg(x < -2)\} \quad (4) $$

with optimum model $\{x \mapsto 6, y \mapsto 2\}$ and cost $= -12$ (Fig. 1c). Now, the only literals opposing to the optimization of cost are $(2x - 3y \le 6)$ and $(y \le 2)$, but none of them can be dropped. Hence, no further improvement can be obtained.

In general, partial truth assignments have an optimum model that is necessarily better or equal to that of the total truth assignments extending them. Since multiple partial truth assignments can be obtained from a total one, the choice of which constraints to drop can be crucial to improve the quality of the optimum model found.

# 4 Exploiting Partial Truth Assignments in OMT

The general schema of our approach is presented in Algorithm 2. This algorithm is a variant of the basic OMT linear-search schema [31, 32] described in Sect. 2.2. The main
**Algorithm 2.** LINEAR-SEARCH OMT WITH PARTIAL ASSIGNMENTS($\varphi$, cost)

**Input:** Formula $\varphi$, objective cost

**Output:** SAT/UNSAT, optimum model $\mathcal{M}$

1: $\mathcal{M} \leftarrow \emptyset$ // Best model found so far

2: ub $\leftarrow \infty$ // Current upper bound

3: res $\leftarrow$ SAT // Status of the search

4: **while** res = SAT **do**

5:     $\langle$res, $\eta\rangle$ $\leftarrow$ SMT.IncrementalSolve($\varphi \land (cost < ub)$)

6:     **if** res = SAT **then**

7:         $\mu$ $\leftarrow$ OMT-REDUCE-ASSIGNMENT($\varphi$, $\eta$, cost)

8:         $\mathcal{M}$ $\leftarrow$ T-Solver.Minimize($\mu$, cost)

9:         ub $\leftarrow \mathcal{M}$(cost)

10: **if** $\mathcal{M} = \emptyset$ **then**

11:     **return** $\langle$UNSAT, $\emptyset\rangle$

12: **else**

13:     **return** $\langle$SAT, $\mathcal{M}\rangle$

difference is the call to the OMT-REDUCE-ASSIGNMENT procedure (line 7), which is responsible for reducing the truth assignment to be fed to the $\mathcal{T}$-minimizer, provided that the resulting partial truth assignment still propositionally satisfies the formula. Depending on the implementation of this procedure, the assignment-reduction strategy can be more or less effective in improving the search for the global optimum.

In Sect. 4.1 and Sect. 4.2, we describe two possible implementations of this procedure.

## 4.1 Basic Assignment Reduction

The first approach is to reduce the truth assignment using Algorithm 1 in Sect. 2.3, i.e., iterating over all the literals in the current truth assignment $\eta$, and dropping them one by one, if possible. A straightforward improvement is to only try to drop $\mathcal{T}$-literals, since they are the ones that, if dropped, can potentially enlarge the area within which the optimum $\mathcal{T}$-model is searched. In the case of theory combination, we drop only literals from the theory $\mathcal{T}$ of the “$\le$” symbol w.r.t. which we minimize. Possibly, heuristics can be used to choose an appropriate dropping order; in our implementation, we used the default strategy that follows the appearance order of the atoms in the formula. This procedure is simple and general, and comes with a limited overhead, as each truth assignment is scanned only once to find the literals to drop, and the $\mathcal{T}$-minimizer is called only once for each candidate assignment.

This approach, however, might not be very effective in practice, as it “blindly” removes literals from the truth assignment without taking into account the properties of the OMT search strategy. In particular, the search space may be enlarged in a direction that does not improve the objective, bringing no benefit to the search. Accurately choosing which literals to drop is crucial because the removal of a literal may prevent the removal of other literals that could potentially be more relevant for the optimization.