Forcing and Interpolation in first-order hybrid Logic with rigid symbols

Daniel G\u{a}in\u{a}; Go Hashimoto

arxiv: 2601.08432 · v2 · submitted 2026-01-13 · 💻 cs.LO

Forcing and Interpolation in first-order hybrid Logic with rigid symbols

Daniel G\u{a}in\u{a} , Go Hashimoto This is my paper

Pith reviewed 2026-05-16 14:52 UTC · model grok-4.3

classification 💻 cs.LO

keywords Craig interpolationfirst-order hybrid logicforcing techniquemany-sorted logicrigid symbolssignature square

0 comments

The pith

A forcing technique that adds constants while preserving consistency proves Craig interpolation for many-sorted first-order hybrid logic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes an analogue of the Craig Interpolation Property for many-sorted first-order hybrid logic with rigid symbols. It introduces a forcing technique that adds new constants to the signature dynamically. This addition preserves consistency even when models have empty domains. The technique leads to general criteria sufficient for signature squares to satisfy the interpolation property. Readers interested in logical foundations for computer science would value this because interpolation supports modular proofs and reasoning.

Core claim

We establish an analogue of Craig Interpolation Property for a many-sorted variant of first-order hybrid logic. We develop a forcing technique that dynamically adds new constants to the underlying signature in a way that preserves consistency, even in the presence of models with possibly empty domains. Using this forcing method, we derive general criteria that are sufficient for a signature square to satisfy Craig interpolation property.

What carries the argument

The forcing technique that dynamically adds new constants to the signature preserving consistency in models possibly with empty domains.

If this is right

Craig interpolation holds for the many-sorted first-order hybrid logic when the signature square meets the derived criteria.
The method works for logics that include rigid symbols.
Consistency holds during forcing even for models with empty domains.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The forcing method could extend to other hybrid or modal logics with similar signature structures.
It may support the construction of interpolation-based decision procedures for verification problems.
Further links to model-theoretic transfer properties in first-order settings remain open for investigation.

Load-bearing premise

The forcing technique dynamically adds new constants to the underlying signature in a way that preserves consistency, even in the presence of models with possibly empty domains.

What would settle it

A specific signature square that meets the general criteria derived from the forcing method yet fails Craig interpolation for some pair of formulas would show the criteria are insufficient.

read the original abstract

In this paper, we establish an analogue of Craig Interpolation Property for a many-sorted variant of first-order hybrid logic. We develop a forcing technique that dynamically adds new constants to the underlying signature in a way that preserves consistency, even in the presence of models with possibly empty domains. Using this forcing method, we derive general criteria that are sufficient for a signature square to satisfy Craig interpolation property.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The forcing technique extends Craig interpolation to many-sorted first-order hybrid logic with rigid symbols and empty domains, but the consistency preservation when adding constants needs explicit verification in the proofs.

read the letter

The main thing here is that the authors give a forcing construction to prove an analogue of Craig interpolation for many-sorted first-order hybrid logic with rigid symbols. They add fresh constants to the signature on the fly while claiming the extension stays consistent even when models can have empty domains, then extract general criteria that are enough for a signature square to satisfy the property. This is a direct technical step beyond earlier interpolation results in modal and hybrid settings, and handling empty domains is a genuine plus because those models appear in applications. The outline is clear and the forcing device looks like the actual new piece of work. The soft spot is the one the stress-test flags. Adding a constant to an empty-domain model normally forces the domain to become non-empty, which would break consistency. The abstract says the method preserves consistency anyway, so the construction must either avoid using the new constants in empty cases or recover the interpolant without them. But no case distinction is mentioned in the general criterion, and without the forcing lemma written out it is hard to see whether the proofs really cover the edge or whether an implicit non-emptiness assumption slipped in. If the details check, the result stands; if not, the criteria would need tightening. This is for logicians working on hybrid logics, proof theory, or verification tools that rely on interpolation. A reader who already knows the modal case will see the extension quickly. It has enough substance and a clear claim to deserve peer review, even if the empty-domain handling will probably require some extra checking or clarification from the authors.

Referee Report

1 major / 1 minor

Summary. The paper claims to establish an analogue of the Craig Interpolation Property for a many-sorted variant of first-order hybrid logic with rigid symbols. It develops a forcing technique that dynamically adds new constants to the underlying signature while preserving consistency even in the presence of models with possibly empty domains, and uses this method to derive general criteria sufficient for a signature square to satisfy the CIP.

Significance. If the forcing construction is rigorously shown to preserve consistency without post-hoc restrictions on empty domains, the result would be a solid technical contribution to the model theory of hybrid logics. It provides a new device for deriving interpolation criteria in the presence of rigid symbols and many-sorted structures, potentially applicable to related modal and hybrid systems. The explicit treatment of signature squares and consistency preservation is a strength when the details hold.

major comments (1)

[Forcing lemma and proof of the general CIP criterion] Forcing lemma and proof of the general CIP criterion: the central construction extends the signature by fresh constants while claiming to preserve consistency even for models with possibly empty domains. In semantics permitting empty domains, a constant symbol must be interpreted by a domain element, so adjoining any constant renders an empty-domain model inconsistent. The manuscript must demonstrate either that the forcing step never requires populating a previously empty domain or that the interpolant can be recovered without the added constants in the empty case; no such case distinction is stated in the general criterion for signature squares. This point is load-bearing for the abstract's claim.

minor comments (1)

The abstract states the method clearly, but the full text would benefit from an explicit preliminary section recalling the semantics of rigid symbols and the precise definition of empty-domain models to aid readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and for identifying this important technical point concerning the interaction between the forcing construction and empty domains. We agree that the current presentation would benefit from greater explicitness on this matter to fully support the claims in the abstract and the general criterion. We address the comment below and will revise the manuscript accordingly.

read point-by-point responses

Referee: Forcing lemma and proof of the general CIP criterion: the central construction extends the signature by fresh constants while claiming to preserve consistency even for models with possibly empty domains. In semantics permitting empty domains, a constant symbol must be interpreted by a domain element, so adjoining any constant renders an empty-domain model inconsistent. The manuscript must demonstrate either that the forcing step never requires populating a previously empty domain or that the interpolant can be recovered without the added constants in the empty case; no such case distinction is stated in the general criterion for signature squares. This point is load-bearing for the abstract's claim.

Authors: We acknowledge that the referee's observation is correct and that the manuscript does not currently contain an explicit case distinction for empty domains within the statement of the general CIP criterion. In the revised version we will add the following clause to the general criterion: if every model of the relevant theories has an empty domain, then the interpolant is recovered directly from the base logic without applying the forcing step (hence without adjoining constants). In all other cases the forcing construction proceeds only on non-empty domains, preserving consistency by the existing lemma. This case distinction will be inserted both in the statement of the criterion and in the proof of the forcing lemma, together with a short verification that the empty-domain case is vacuously consistent with the signature square. We believe these additions fully address the concern while leaving the core technical results unchanged. revision: yes

Circularity Check

0 steps flagged

No circularity in forcing-based derivation of CIP criteria

full rationale

The paper introduces a forcing technique that dynamically extends signatures by fresh constants while preserving consistency, including for models with possibly empty domains, then applies it to obtain sufficient conditions on signature squares for the Craig interpolation property in many-sorted first-order hybrid logic. No load-bearing step reduces by construction to its own inputs: the forcing construction is presented as an independent technical device whose consistency preservation is asserted directly from the semantics rather than derived from the target interpolation result, and no self-citation, fitted parameter, or ansatz is invoked to close the derivation. The central claims therefore remain self-contained against the external semantics of hybrid logic.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard background axioms of first-order hybrid logic and the many-sorted signature framework with rigid symbols; the forcing construction is the primary new device. No free parameters or invented entities are mentioned in the abstract.

axioms (2)

standard math Standard axioms and semantics of first-order hybrid logic
The logic variant is defined as an extension of known hybrid logic.
domain assumption Many-sorted signatures allowing rigid symbols and possibly empty domains
Explicitly stated as part of the variant considered.

pith-pipeline@v0.9.0 · 5350 in / 1101 out tokens · 29507 ms · 2026-05-16T14:52:07.375045+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We develop a forcing technique that dynamically adds new constants to the underlying signature in a way that preserves consistency, even in the presence of models with possibly empty domains.
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat.equivNat unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Theorem 52 (Interpolation). ... If the span lifts quasi-isomorphisms then the pushout has CIP.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages

[1]

Hybrid-Dynamic Ehrenfeucht-Fraïssé Games.ACM Trans

4 Guillermo Badia, Daniel Găină, Alexander Knapp, Tomasz Kowalski, and Martin Wirsing. Hybrid-Dynamic Ehrenfeucht-Fraïssé Games.ACM Trans. Comput. Logic, 26(4), September 2025.doi:10.1145/3750046. 5 Jan A. Bergstra, Jan Heering, and Paul Klint. Module algebra.J. ACM, 37(2):335–372,

work page doi:10.1145/3750046 2025
[2]

doi:10.1145/77600.77621. D. Găină and G. Hashimoto 37 6 Patrick Blackburn, Manuel A. Martins, María Manzano, and Antonia Huertas. Rigid first-order hybrid logic. In Rosalie Iemhoff, Michael Moortgat, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Jul...

work page doi:10.1145/77600.77621 2019
[3]

7 Tomasz Borzyszkowski

Springer. 7 Tomasz Borzyszkowski. Generalized interpolation in CASL.Information Processing Letters, 76(1-2):19–24, 2000.doi:10.1016/S0020-0190(00)00120-4. 8 Tomasz Borzyszkowski. Logical systems for structured specifications.Theoretical Computer Science, 286(2):197–245,

work page doi:10.1016/s0020-0190(00)00120-4 2000
[4]

Hybridisation of institutions in HETS (tool paper)

9 Mihai Codescu. Hybridisation of institutions in HETS (tool paper). In Markus Roggenbach and Ana Sokolova, editors,8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019, June 3-6, 2019, London, United Kingdom, volume 139 ofLIPIcs, pages 17:1–17:10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,

work page 2019
[5]

Linear Reasoning

10 William Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem.Journal of Symbolic Logic, 22(3):250–268, 1957.doi:10.2307/2963593. 11 Răzvan Diaconescu.Institution-Independent Model Theory. Studies in Universal Logic. Birkhäuser,

work page doi:10.2307/2963593 1957
[6]

Implicit kripke semantics and ultraproducts in stratified institutions.J

12 Razvan Diaconescu. Implicit kripke semantics and ultraproducts in stratified institutions.J. Log. Comput., 27(5):1577–1606, 2017.doi:10.1093/LOGCOM/EXW018. 13 Răzvan Diaconescu. Institution-independent Ultraproducts.Fundamenta Informaticæ, 55(3- 4):321–348,

work page doi:10.1093/logcom/exw018 2017
[7]

Completeness of many-sorted equational logic.ACM SIGPLAN Notices, 17(1):9–17, 1982.doi:10.1145/947886.947887

17 Joseph Goguen and José Meseguer. Completeness of many-sorted equational logic.ACM SIGPLAN Notices, 17(1):9–17, 1982.doi:10.1145/947886.947887. 18 Joseph A. Goguen and Rod M. Burstall. Institutions: Abstract model theory for specification and programming.J. ACM, 39(1):95–146, 1992.doi:10.1145/147508.147524. 19 Daniel Găină. Foundations of logic programm...

work page doi:10.1145/947886.947887 1982
[8]

Forcing and calculi for hybrid logics.Journal of the Association for Computing Machinery, 67(4):1–55, 2020.doi:10.1145/3400294

20 Daniel Găină. Forcing and calculi for hybrid logics.Journal of the Association for Computing Machinery, 67(4):1–55, 2020.doi:10.1145/3400294. 21 Daniel Găină, Guillermo Badia, and Tomasz Kowalski. Robinson consistency in many-sorted hybrid first-order logics. In David Fernández-Duque, Alessandra Palmigiano, and Sophie Pinchinat, editors,Advances in Mod...

work page doi:10.1145/3400294 2020
[9]

Omitting types theorem in hybrid dynamic first-order logic with rigid symbols.Annals of Pure and Applied Logic, 174(3):103212, 2023.doi:10.1016/J.APAL.2022.103212

22 Daniel Găină, Guillermo Badia, and Tomasz Kowalski. Omitting types theorem in hybrid dynamic first-order logic with rigid symbols.Annals of Pure and Applied Logic, 174(3):103212, 2023.doi:10.1016/J.APAL.2022.103212. 23 Daniel Găină and Andrei Popescu. An institution-independent proof of the Robinson consist- ency theorem.Studia Logica, 85(1):41–73, 200...

work page doi:10.1016/j.apal.2022.103212 2023
[10]

25 Go Hashimoto, Daniel Găină, and Ionut Ţuţu

Schloss Dagstuhl – Leibniz-Zentrum für Informatik.doi:10.4230/LIPIcs.MFCS.2025.55. 25 Go Hashimoto, Daniel Găină, and Ionut Ţuţu. Forcing, Transition Algebras, and Calculi. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors,51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn,...

work page doi:10.4230/lipics.mfcs.2025.55 2025
[11]

27 T. S. E. Maibaum, M. R. Sadler, and Paulo A. S. Veloso. Logical specification and implementa- tion. In Mathai Joseph and R. K. Shyamasundar, editors,Foundations of Software Technology and Theoretical Computer Science, Fourth Conference, Bangalore, India, December 13-15, 1984, Proceedings, volume 181 ofLecture Notes in Computer Science, pages 13–30. Spr...

work page doi:10.1007/3-540-13883-8 1984
[12]

29 Marius Petria

Springer. 29 Marius Petria. An institutional version of Gödel’s completeness theorem. In Till Mos- sakowski, Ugo Montanari, and Magne Haveraaen, editors,Algebra and Coalgebra in Com- puter Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 ofLNCS, pages 409–424. Springer,

work page 2007
[13]

30 Abraham Robinson

doi: 10.1007/978-3-540-73859-6\_28. 30 Abraham Robinson. A result on consistency and its application to the theory of definition. Indagationes Mathematicae (Proceedings), 59:47–58,

work page doi:10.1007/978-3-540-73859-6
[14]

com/science/article/pii/S138572585650008X,doi:10.1016/S1385-7258(56)50008-X

URL:https://www.sciencedirect. com/science/article/pii/S138572585650008X,doi:10.1016/S1385-7258(56)50008-X. 31 Donald Sannella and Andrzej Tarlecki. Property-oriented semantics of structured specifications. Math. Struct. Comput. Sci., 24(2), 2014.doi:10.1017/S0960129513000212. 32 Andrzej Tarlecki. Bits and pieces of the theory of institutions. In Klaus Dr...

work page doi:10.1016/s1385-7258(56)50008-x 2014
[15]

On the fragility of interpolation.The Journal of Symbolic Logic, FirstView:1– 38, 2024.doi:10.1017/jsl.2024.19

33 Andrzej Tarlecki. On the fragility of interpolation.The Journal of Symbolic Logic, FirstView:1– 38, 2024.doi:10.1017/jsl.2024.19. 34 Paulo A. S. Veloso. On pushout consistency, modularity and interpolation for logical specifica- tions.Inf. Process. Lett., 60(2):59–66, 1996.doi:10.1016/S0020-0190(96)00146-9. 35 Paulo A. S. Veloso and T. S. E. Maibaum. O...

work page doi:10.1017/jsl.2024.19 2024
[16]

doi:10.1016/0020-0190(94)00203-B

work page doi:10.1016/0020-0190(94)00203-b

[1] [1]

Hybrid-Dynamic Ehrenfeucht-Fraïssé Games.ACM Trans

4 Guillermo Badia, Daniel Găină, Alexander Knapp, Tomasz Kowalski, and Martin Wirsing. Hybrid-Dynamic Ehrenfeucht-Fraïssé Games.ACM Trans. Comput. Logic, 26(4), September 2025.doi:10.1145/3750046. 5 Jan A. Bergstra, Jan Heering, and Paul Klint. Module algebra.J. ACM, 37(2):335–372,

work page doi:10.1145/3750046 2025

[2] [2]

doi:10.1145/77600.77621. D. Găină and G. Hashimoto 37 6 Patrick Blackburn, Manuel A. Martins, María Manzano, and Antonia Huertas. Rigid first-order hybrid logic. In Rosalie Iemhoff, Michael Moortgat, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Jul...

work page doi:10.1145/77600.77621 2019

[3] [3]

7 Tomasz Borzyszkowski

Springer. 7 Tomasz Borzyszkowski. Generalized interpolation in CASL.Information Processing Letters, 76(1-2):19–24, 2000.doi:10.1016/S0020-0190(00)00120-4. 8 Tomasz Borzyszkowski. Logical systems for structured specifications.Theoretical Computer Science, 286(2):197–245,

work page doi:10.1016/s0020-0190(00)00120-4 2000

[4] [4]

Hybridisation of institutions in HETS (tool paper)

9 Mihai Codescu. Hybridisation of institutions in HETS (tool paper). In Markus Roggenbach and Ana Sokolova, editors,8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019, June 3-6, 2019, London, United Kingdom, volume 139 ofLIPIcs, pages 17:1–17:10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,

work page 2019

[5] [5]

Linear Reasoning

10 William Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem.Journal of Symbolic Logic, 22(3):250–268, 1957.doi:10.2307/2963593. 11 Răzvan Diaconescu.Institution-Independent Model Theory. Studies in Universal Logic. Birkhäuser,

work page doi:10.2307/2963593 1957

[6] [6]

Implicit kripke semantics and ultraproducts in stratified institutions.J

12 Razvan Diaconescu. Implicit kripke semantics and ultraproducts in stratified institutions.J. Log. Comput., 27(5):1577–1606, 2017.doi:10.1093/LOGCOM/EXW018. 13 Răzvan Diaconescu. Institution-independent Ultraproducts.Fundamenta Informaticæ, 55(3- 4):321–348,

work page doi:10.1093/logcom/exw018 2017

[7] [7]

Completeness of many-sorted equational logic.ACM SIGPLAN Notices, 17(1):9–17, 1982.doi:10.1145/947886.947887

17 Joseph Goguen and José Meseguer. Completeness of many-sorted equational logic.ACM SIGPLAN Notices, 17(1):9–17, 1982.doi:10.1145/947886.947887. 18 Joseph A. Goguen and Rod M. Burstall. Institutions: Abstract model theory for specification and programming.J. ACM, 39(1):95–146, 1992.doi:10.1145/147508.147524. 19 Daniel Găină. Foundations of logic programm...

work page doi:10.1145/947886.947887 1982

[8] [8]

Forcing and calculi for hybrid logics.Journal of the Association for Computing Machinery, 67(4):1–55, 2020.doi:10.1145/3400294

20 Daniel Găină. Forcing and calculi for hybrid logics.Journal of the Association for Computing Machinery, 67(4):1–55, 2020.doi:10.1145/3400294. 21 Daniel Găină, Guillermo Badia, and Tomasz Kowalski. Robinson consistency in many-sorted hybrid first-order logics. In David Fernández-Duque, Alessandra Palmigiano, and Sophie Pinchinat, editors,Advances in Mod...

work page doi:10.1145/3400294 2020

[9] [9]

Omitting types theorem in hybrid dynamic first-order logic with rigid symbols.Annals of Pure and Applied Logic, 174(3):103212, 2023.doi:10.1016/J.APAL.2022.103212

22 Daniel Găină, Guillermo Badia, and Tomasz Kowalski. Omitting types theorem in hybrid dynamic first-order logic with rigid symbols.Annals of Pure and Applied Logic, 174(3):103212, 2023.doi:10.1016/J.APAL.2022.103212. 23 Daniel Găină and Andrei Popescu. An institution-independent proof of the Robinson consist- ency theorem.Studia Logica, 85(1):41–73, 200...

work page doi:10.1016/j.apal.2022.103212 2023

[10] [10]

25 Go Hashimoto, Daniel Găină, and Ionut Ţuţu

Schloss Dagstuhl – Leibniz-Zentrum für Informatik.doi:10.4230/LIPIcs.MFCS.2025.55. 25 Go Hashimoto, Daniel Găină, and Ionut Ţuţu. Forcing, Transition Algebras, and Calculi. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors,51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn,...

work page doi:10.4230/lipics.mfcs.2025.55 2025

[11] [11]

27 T. S. E. Maibaum, M. R. Sadler, and Paulo A. S. Veloso. Logical specification and implementa- tion. In Mathai Joseph and R. K. Shyamasundar, editors,Foundations of Software Technology and Theoretical Computer Science, Fourth Conference, Bangalore, India, December 13-15, 1984, Proceedings, volume 181 ofLecture Notes in Computer Science, pages 13–30. Spr...

work page doi:10.1007/3-540-13883-8 1984

[12] [12]

29 Marius Petria

Springer. 29 Marius Petria. An institutional version of Gödel’s completeness theorem. In Till Mos- sakowski, Ugo Montanari, and Magne Haveraaen, editors,Algebra and Coalgebra in Com- puter Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 ofLNCS, pages 409–424. Springer,

work page 2007

[13] [13]

30 Abraham Robinson

doi: 10.1007/978-3-540-73859-6\_28. 30 Abraham Robinson. A result on consistency and its application to the theory of definition. Indagationes Mathematicae (Proceedings), 59:47–58,

work page doi:10.1007/978-3-540-73859-6

[14] [14]

com/science/article/pii/S138572585650008X,doi:10.1016/S1385-7258(56)50008-X

URL:https://www.sciencedirect. com/science/article/pii/S138572585650008X,doi:10.1016/S1385-7258(56)50008-X. 31 Donald Sannella and Andrzej Tarlecki. Property-oriented semantics of structured specifications. Math. Struct. Comput. Sci., 24(2), 2014.doi:10.1017/S0960129513000212. 32 Andrzej Tarlecki. Bits and pieces of the theory of institutions. In Klaus Dr...

work page doi:10.1016/s1385-7258(56)50008-x 2014

[15] [15]

On the fragility of interpolation.The Journal of Symbolic Logic, FirstView:1– 38, 2024.doi:10.1017/jsl.2024.19

33 Andrzej Tarlecki. On the fragility of interpolation.The Journal of Symbolic Logic, FirstView:1– 38, 2024.doi:10.1017/jsl.2024.19. 34 Paulo A. S. Veloso. On pushout consistency, modularity and interpolation for logical specifica- tions.Inf. Process. Lett., 60(2):59–66, 1996.doi:10.1016/S0020-0190(96)00146-9. 35 Paulo A. S. Veloso and T. S. E. Maibaum. O...

work page doi:10.1017/jsl.2024.19 2024

[16] [16]

doi:10.1016/0020-0190(94)00203-B

work page doi:10.1016/0020-0190(94)00203-b