[1] F. Baader, S. Ghilardi, Unification in modal and description logics, Logic Journal of the IGPL. Interest
Group in Pure and Applied Logics, 19(6) (2011), 705–730.
[2] G. Bezhanishvili, N. Bezhanishvili, L. Carai, D. Gabelaia, S. Ghilardi, M. Jibladze, Diego’s theorem for
nuclear implicative semilattices, Koninklijke Nederlandse Akademie van Wetenschappen. Indagationes
Mathematicae. New Series, 32(2) (2021), 498–535.
[3] G. Bezhanishvili, N. Bezhanishvili, J. Ilin, Subframization and stabilization for superintuitionistic logics,
Journal of Logic and Computation, 29(1) (2019), 1–35.
[4] G. Bezhanishvili, S. Ghilardi, An algebraic approach to subframe logics. Intuitionistic case, Annals of
Pure and Applied Logic, 147(1-2) (2007), 84–100.
[5] S. Bozzi, G.C. Meloni, Completezza proposizionale per l’operatore modale ”accade localmente che”,
Bollettino della Unione Matematica Italiana, A. Serie 5, 14(3) (1977), 489–497.
[6] S. Bozzi, G.C. Meloni, Representation of Heyting algebras with covering and propositional intuitionistic
logic with local operator, Bollettino della Unione Matematica Italiana, A. Serie 5, 17(3) (1980), 436–442.
[7] S.A. Celani, D. Montangie, Algebraic semantics of the {→,□}-fragment of propositional lax logic, Soft
Computing, 24(2) (2020), 813–823.
[8] U. Egly, Embedding lax logic into intuitionistic logic, Automated Deduction - CADE-18, 18th International
Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings,
Lecture Notes in Computer Science, (2002), 78–93.
[9] M. Fairtlough, M. Mendler, Propositional lax logic, Information and Computation, 137(1) (1997), 1–33.
[10] M. Fairtlough, M. Mendler, X. Cheng, Abstraction and refinement in higher order logic, Theorem
Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland,
UK, September 3-6, 2001, Proceedings, Springer, (2001), 201–216.
[11] S. Ghilardi, Unification in intuitionistic logic, The Journal of Symbolic Logic, 64(2) (1999), 859–880.
[12] S. Ghilardi, Best solving modal equations, Annals of Pure and Applied Logic, 102(3) (2000), 183–198.
[13] S. Ghilardi, A resolution/tableaux algorithm for projective approximations in IPC, Logic Journal of the
IGPL. Interest Group in Pure and Applied Logics, 10(3) (2002), 229–243.
[14] S. Ghilardi, G.C. Meloni, Modelli con coperture per la logica proposizionale intuizionista e locale,
Universitá degli Studi di Siena, (1985), 333-338.
[15] S. Ghilardi, M. Zawadowski, Sheaves, games, and model completions, Kluwer Academic Publishers,
Dordrecht, (2002), x+243.
[16] R.I. Goldblatt, Grothendieck topology as geometric modality, Zeitschrift für Mathematische Logik und
Grundlagen der Mathematik, 27(6) (1981), 495–529.
[17] J.M. Howe, Proof search in lax logic, Mathematical Structures in Computer Science. A Journal in the
Applications of Categorical, Algebraic and Geometric Methods in Computer Science, 11(4) (2001),
573–588.
[18] E. Jeřábek, Complexity of admissible rules, Archive for Mathematical Logic, 46(2) (2007), 73–92.
[19] E. Jeřábek, Blending margins: The modal logic K has nullary unification type, Journal of Logic and
Computation, 25(5) (2015), 1231–1240.
[20] E. Jeřábek, Rules with parameters in modal logic II, Annals of Pure and Applied Logic, 171(10) (2020),
102829, 59.
[21] P.T. Johnstone, Stone spaces, Cambridge University Press, Cambridge, (1986), xxii+370.
[22] F.W. Lawvere, Introduction: Toposes, algebraic geometry and logic (Conf., Dalhousie Univ., Halifax,
N.S., 1971), Lecture Notes in Mathematics, 274 (1972), 1–12.
[23] R. Lemhoff, G. Metcalfe, Proof theory for admissible rules, Annals of Pure and Applied Logic, 159(1-2)
(2009), 171–186.
[24] M. Mendler, Constrained proofs: A logic for dealing with behavioural constraints in formal hardware
verification, Designing Correct Circuits, Springer, (1990), 1–28.
[25] M. Mendler, A timing refinement of intuitionistic proofs and its application to the timing analysis of
combinational circuits, Theorem proving with analytic tableaux and related methods, 5th International
Workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15-17, Springer, 1996.
[26] G. Mints, A short introduction to intuitionistic logic, The University Series in Mathematics, Kluwer
Academic/Plenum Publishers, New York, 2000.
[27] F. Pfenning, R. Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer
Science, 11(4) (2001), 511–540.
[28] M. Tierney, Forcing topologies and classifying topoi, Algebra, Topology, and Category Theory (a collection
of papers in honor of Samuel Eilenberg), (1976), 211–219.
[29] B. Veit, A proof of the associated sheaf theorem by means of categorical logic, The Journal of Symbolic
Logic, 46(1) (1981), 45–55
)
