More Web Proxy on the site http://driver.im/

research-article

Forcing and Calculi for Hybrid Logics

Author:

Daniel GăinăAuthors Info & Claims

Journal of the ACM (JACM), Volume 67, Issue 4

Article No.: 25, Pages 1 - 55

https://doi.org/10.1145/3400294

Published: 06 August 2020 Publication History

Abstract

The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research, such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedical informatics, semantic networks, and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. To prove completeness, the article introduces a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems.

References

[1]

Marc Aiguier and Razvan Diaconescu. 2007. Stratified institutions and elementary homomorphisms. Info. Process. Lett. 103, 1 (2007), 5--13.

Digital Library

[2]

Carlos Areces and Patrick Blackburn. 2001. Bringing them all together. J. Logic Comput. 11, 5 (2001), 657--669.

[3]

Egidio Astesiano, Michel Bidoit, Hélène Kirchner, Bernd Krieg-Brückner, Peter D. Mosses, Donald Sannella, and Andrzej Tarlecki. 2002. CASL: The common algebraic specification language. Theoret. Comput. Sci. 286, 2 (2002), 153--196.

Digital Library

[4]

Franz Baader, Ian Horrocks, Carsten Lutz, and Uli Sattler. 2017. An Introduction to Description Logic. Cambridge University Press.

[5]

Jon Barwise. 1970. Notes on forcing and countable fragments (unpublished).

[6]

Jean-Yves Béziau. 2006. 13 questions about universal logic. Bull. Sect. Logic 35, 2/3 (2006), 133--150.

[7]

Jean-Yves Béziau. 2012. Universal Logic: An Anthology: From Paul Hertz to Dov Gabbay. Birkhäuser, Basel.

[8]

Patrick Blackburn. 2000. Representation, reasoning, and relational structures: A hybrid logic manifesto. Logic J. IGPL 8, 3 (2000), 339--365.

[9]

Patrick Blackburn, Manuel A. Martins, María Manzano, and Antonia Huertas. 2019. Rigid first-order hybrid logic. In Proceedings of the 26th International Workshop on Logic, Language, Information, and Computation (WoLLIC’19) (Lecture Notes in Computer Science), Rosalie Iemhoff, Michael Moortgat, and Ruy J. G. B. de Queiroz (Eds.), Vol. 11541. Springer, 53--69.

[10]

Patrick Blackburn and Maarten Marx. 2002. Tableaux for quantified hybrid logic. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’02) (Lecture Notes in Computer Science), Uwe Egly and Christian G. Fermüller (Eds.), Vol. 2381. Springer, 38--52.

[11]

Torben Braüner. 2011. Hybrid Logic and Its Proof-Theory. Applied Logic Series, Vol. 37. Springer, Netherlands.

[12]

Mihai Codescu. 2019. Hybridisation of institutions in HETS (tool paper). In Proceedings of the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO’19), Markus Roggenbach and Ana Sokolova (Eds.), Vol. 139. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 17:1--17:10.

[13]

Mihai Codescu and Daniel Găină. 2008. Birkhoff completeness in institutions. Logica Universalis 2, 2 (2008), 277--309.

[14]

Paul J. Cohen. 1963. The independence of the continuum hypothesis. Proc. Natl. Acad. Sci. U.S.A. 50, 6 (Dec. 1963), 1143--1148.

[15]

Paul J. Cohen. 1964. The independence of the continuum hypothesis, II. Proc. Natl. Acad. Sci. U.S.A. 51, 1 (Jan. 1964), 105--110.

[16]

Ionuţ Ţutu and José Luiz Fiadeiro. 2017. From conventional to institution-independent logic programming. J. Logic Comput. 27, 6 (2017), 1679--1716.

[17]

Răzvan Diaconescu. 2003. Institution-independent ultraproducts. Fundamenta Informaticæ 55, 3–4 (2003), 321--348.

[18]

Răzvan Diaconescu. 2004. An institution-independent proof of craig interpolation theorem. Studia Logica 77, 1 (2004), 59--79.

[19]

Razvan Diaconescu. 2004. Elementary diagrams in institutions. J. Logic Comput. 14, 5 (2004), 651--674.

Digital Library

[20]

Razvan Diaconescu. 2004. Herbrand theorems in arbitrary institutions. Info. Process. Lett. 90, 1 (2004), 29--37.

Digital Library

[21]

Răzvan Diaconescu. 2006. Proof systems for institutional logic. J. Logic Comput. 16, 3 (2006), 339--357.

Digital Library

[22]

Răzvan Diaconescu. 2008. Institution-independent Model Theory (1 ed.). Birkhäuser, Basel.

[23]

Răzvan Diaconescu. 2016. Quasi-varieties and initial semantics for hybridized institutions. J. Logic Comput. 26, 3 (2016), 855--891.

[24]

Razvan Diaconescu. 2017. Implicit Kripke semantics and ultraproducts in stratified institutions. J. Logic Comput. 27, 5 (2017), 1577--1606.

[25]

Razvan Diaconescu and Kokichi Futatsugi. 2002. Logical foundations of CafeOBJ. Theoret. Comput. Sci. 285, 2 (2002), 289--318.

Digital Library

[26]

Răzvan Diaconescu and Alexandre Madeira. 2016. Encoding hybridised institutions into first-order logic. Math. Struct. Comput. Sci. 26, 5 (2016), 745--788.

[27]

Razvan Diaconescu and Marius Petria. 2010. Saturated models in institutions. Arch. Math. Log. 49, 6 (2010), 693--723.

[28]

Razvan Diaconescu and Petros S. Stefaneas. 2007. Ultraproducts and possible worlds semantics in institutions. Theoret. Comput. Sci. 379, 1–2 (2007), 210--230.

Digital Library

[29]

Marcelo Finger and Dov M. Gabbay. 1992. Adding a temporal dimension to a logic system. J. Logic Lang. Info. 1, 3 (Sep. 1992), 203--233.

[30]

Melvin Fitting and Richard L. Mendelsohn. 1998. First-Order Modal Logic. Kluwer Academic Publishers.

[31]

Joseph Goguen and Rod Burstall. 1992. Institutions: Abstract model theory for specification and programming. J. Assoc. Comput. Mach. 39, 1 (1992), 95--146.

Digital Library

[32]

Joseph A. Goguen and José Meseguer. 1992. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105, 2 (1992), 217--273.

Digital Library

[33]

Daniel Găină. 2013. Interpolation in logics with constructors. Theoret. Comput. Sci. 474 (2013), 46--59.

Digital Library

[34]

Daniel Găină. 2014. Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally. Logica Universalis 8, 3-4 (2014), 469--498.

[35]

Daniel Găină. 2015. Foundations of logic programming in hybridised logics. In Proceedings of the 22nd International Workshop on Recent Trends in Algebraic Development Techniques (WADT’14) (Lecture Notes in Computer Science), Mihai Codescu, Răzvan Diaconescu, and Ionuţ Ţuţu (Eds.), Vol. 9463. Springer, 69--89.

Digital Library

[36]

Daniel Găină. 2017. Birkhoff style calculi for hybrid logics. Formal Asp. Comput. 29, 5 (2017), 805--832.

Digital Library

[37]

Daniel Găină. 2017. Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors. J. Logic Comput. 27, 6 (2017), 1717--1752.

[38]

Daniel Găină. 2017. Foundations of logic programming in hybrid logics with user-defined sharing. Theor. Comput. Sci. 686 (2017), 1--24.

[39]

Daniel Găină and Ionut Ţuţu. 2019. Birkhoff completeness for hybrid-dynamic first-order logic. In Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’19) (Lecture Notes in Computer Science), Serenella Cerrito and Andrei Popescu (Eds.), Vol. 11714. Springer, 277--293.

[40]

Daniel Găină and Kokichi Futatsugi. 2015. Initial semantics in logics with constructors. J. Logic Comput. 25, 1 (2015), 95--116.

[41]

Daniel Găină, Kokichi Futatsugi, and Kazuhiro Ogata. 2012. Constructor-based logics. J. UCS 18, 16 (2012), 2204--2233.

[42]

Daniel Găină and Marius Petria. 2010. Completeness by forcing. J. Logic Comput. 20, 6 (2010), 1165--1186.

Digital Library

[43]

Daniel Găină and Andrei Popescu. 2006. An institution-independent generalization of Tarski’s elementary chain theorem. J. Logic Comput. 16, 6 (2006), 713--735.

[44]

Daniel Găină and Andrei Popescu. 2007. An institution-independent proof of robinson consistency theorem. Studia Logica 85, 1 (2007), 41--73.

[45]

Joseph Y. Halpern and Yoav Shoham. 1991. A propositional modal logic of time intervals. J. ACM 38, 4 (1991), 935--962.

Digital Library

[46]

Wilfrid Hodges. 1993. Model Theory. Cambridge University Press, UK.

[47]

H. Jerome Keisler. 1973. Forcing and the omitting types theorem. In Studies in Model Theory, M. D. Morley (Ed.), Vol. 8. Math. Assoc. Amer, New York, 96--133.

[48]

Saunders MacLane. 1998. Categories for the Working Mathematician. Springer-Verlag, New York.

[49]

Alexandre Madeira, Manuel A. Martins, Luís Soares Barbosa, and Rolf Hennicker. 2015. Refinement in hybridised institutions. Formal Aspects Comput. 27, 2 (2015), 375--395.

Digital Library

[50]

Manuel A. Martins, Alexandre Madeira, Razvan Diaconescu, and Luís Soares Barbosa. 2011. Hybridization of institutions. In Proceedings of the 4th International Conference on Algebra and Coalgebra in Computer Science (CALCO’11) (Lecture Notes in Computer Science), Andrea Corradini, Bartek Klin, and Corina Cîrstea (Eds.), Vol. 6859. Springer, 283--297.

[51]

Joseph Meseguer. 1989. General logics. In Proceedings of the Logic Colloquium ’87, H.-D. Ebbinghaus, J. Fernandez-Prida, M. Garrido, D. Lascar, and M. Rodriguez Artalejo (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 129. North Holland, 275--329.

[52]

José Meseguer. 1997. Membership algebra as a logical framework for equational specification. In Proceedings of the 12th International Workshop on Recent Trends in Algebraic Development Techniques (WADT’97) (Lecture Notes in Computer Science), Francesco Parisi-Presicce (Ed.), Vol. 1376. Springer, 18--61.

[53]

Bernhard Möller, Andrzej Tarlecki, and Martin Wirsing. 1987. Algebraic specifications of reachable higher-order algebras. In Proceedings of the International Conference on Algorithmic Decision Theory (ADT’87) (Lecture Notes in Computer Science), Donald Sannella and Andrzej Tarlecki (Eds.), Vol. 332. Springer, 154--169.

[54]

Till Mossakowski, Razvan Diaconescu, and Andrzej Tarlecki. 2009. What is a logic translation? Logica Universalis 3, 1 (2009), 95--124.

[55]

Till Mossakowski, Anne Elisabeth Haxthausen, Donald Sannella, and Andrzej Tarlecki. 2003. CASL—The common algebraic specification language: Semantics and proof theory. Comput. Artific. Intell. 22, 3-4 (2003), 285--321.

[56]

Till Mossakowski, Christian Maeder, and Klaus Lüttich. 2007. The heterogeneous tool set (hets). In Proceedings of 4th International Verification Workshop in connection with CADE-21 (CEUR Workshop Proceedings), Bernhard Beckert (Ed.), Vol. 259. Retrieved from CEUR-WS.org.

[57]

Renato Neves, Alexandre Madeira, Manuel A. Martins, and Luís Soares Barbosa. 2016. Proof theory for hybrid(ised) logics. Sci. Comput. Program. 126 (2016), 73--93.

Digital Library

[58]

Renato Neves, Manuel A. Martins, and Luís Soares Barbosa. 2014. Completeness and decidability results for hybrid(ised) logics. In Proceedings of the 17th Brazilian Symposium on Formal Methods: Foundations and Applications (SBMF’14) (Lecture Notes in Computer Science), Christiano Braga and Narciso Martí-Oliet (Eds.), Vol. 8941. Springer, 146--161.

[59]

Solomon Passay and Tinko Tinchev. 1991. An essay in combinatory dynamic logic. Info. Comput. 93, 2 (1991), 263--332.

[60]

Marius Petria. 2007. An institutional version of Gödel’s completeness theorem. In Proceedings of the 2nd International Conference on Algebra and Coalgebra in Computer Science (CALCO’07) (Lecture Notes in Computer Science), Till Mossakowski, Ugo Montanari, and Magne Haveraaen (Eds.), Vol. 4624. Springer, 409--424.

[61]

Marius Petria and Răzvan Diaconescu. 2006. Abstract Beth definability in institutions. J. Symbol. Logic 71, 3 (2006), 1002--1028.

[62]

Arthur Prior. 1967. Past, Present and Future. Oxford University Press, Oxford.

[63]

Joseph R. Shoenfield. 1967. Mathematical Logic. Addison-Wesley, Reading, MA.

[64]

Abraham Robinson. 1971. Forcing in model theory. Symp. Math. 5 (1971), 69--82.

[65]

William C. Rounds. 1997. Chapter 8—Feature logics. In Handbook of Logic and Language, Johan van Benthem and Alice ter Meulen (Eds.). North-Holland, Amsterdam, 475--533.

[66]

Donald Sannella and Andrzej Tarlecki. 1988. Specifications in an arbitrary institution. Info. Comput. 76, 2/3 (1988), 165--210.

Digital Library

[67]

Gerhard Schurz. 2011. Combinations and completeness transfer for quantified modal logics. Logic Journal of the IGPL 19, 4 (2011), 598--616.

[68]

Robert Szepesia and Horia Ciocârlie. 2011. An overview on software reconfiguration. Theory Appl. Math. Comput. Sci. 1, 1 (2011), 74--79.

[69]

Andrzej Tarlecki. 1985. On the existence of free models in abstract algebraic institutions. Theor. Comput. Sci. 37 (1985), 269--304.

[70]

Andrzej Tarlecki. 1986. Bits and pieces of the theory of institutions. In Proceedings of the Summer Workshop on Category Theory and Computer Programming (Lecture Notes in Computer Science), David Pitt, Samson Abramsky, Axel Poigné, and David Rydeheard (Eds.). Vol. 240. Springer, 334--360.

[71]

Andrzej Tarlecki. 1986. Quasi-varieties in abstract algebraic institutions. J. Comput. System Sci. 33, 3 (1986), 333--360.

Digital Library

[72]

Ionut Tutu, Claudia Elena Chirita, Antónia Lopes, and José Luiz Fiadeiro. 2019. Logical support for bike-sharing system design. In Proceedings From Software Engineering to Formal Methods and Tools, and Back—Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday (Lecture Notes in Computer Science), Maurice H. ter Beek, Alessandro Fantechi, and Laura Semini (Eds.), Vol. 11865. Springer, 152--171.

[73]

Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobalt, and Dalibor Topic. 2002. SPASS Version 2.0. In Proceedings of the 18th International Conference on Automated Deduction (CADE’02) (Lecture Notes in Computer Science), Andrei Voronkov (Ed.), Vol. 2392. Springer, 275--279.

Cited By

Găină DBadia GKowalski T(2023)Omitting types theorem in hybrid dynamic first-order logic with rigid symbolsAnnals of Pure and Applied Logic10.1016/j.apal.2022.103212174:3(103212)Online publication date: Mar-2023
https://doi.org/10.1016/j.apal.2022.103212
Diaconescu R(2022)The Axiomatic Approach to Non-Classical Model TheoryMathematics10.3390/math1019342810:19(3428)Online publication date: 21-Sep-2022
https://doi.org/10.3390/math10193428
Diaconescu R(2022)Representing 3/2-Institutions as Stratified InstitutionsMathematics10.3390/math1009150710:9(1507)Online publication date: 1-May-2022
https://doi.org/10.3390/math10091507
Show More Cited By

Index Terms

Forcing and Calculi for Hybrid Logics
1. Theory of computation
  1. Logic

Recommendations

Labelled Sequent Calculi for Inquisitive Modal Logics
Logic, Language, Information, and Computation
Abstract
We present cut-free labelled sequent calculi for various systems of inquisitive modal logic, including inquisitive epistemic logic and inquisitive doxastic logic. Inquisitive modal logic extends the framework of standard modal logic with a ...
Birkhoff style calculi for hybrid logics
Abstract
We develop an abstract proof calculus for hybrid logics whose sentences are (hybrid) Horn clauses, and we prove a Birkhoff completeness theorem for hybrid logics in the general setting provided by the institution theory. This result is then ...
Terminating Tableau Calculi for Hybrid Logics Extending K

This article builds on work by Bolander and Blackburn [Thomas Bolander and Patrick Blackburn. Termination for hybrid tableaus. Journal of Logic and Computation, 17(3):517-554, 2007] on terminating tableau systems for the minimal hybrid logic K. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 67, Issue 4

August 2020

265 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/3403612

Editor:
Éva Tardos
Cornell University

Issue’s Table of Contents

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 August 2020

Accepted: 01 May 2020

Revised: 01 March 2020

Received: 01 August 2018

Published in JACM Volume 67, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
145
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)1

Reflects downloads up to 14 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Găină DBadia GKowalski T(2023)Omitting types theorem in hybrid dynamic first-order logic with rigid symbolsAnnals of Pure and Applied Logic10.1016/j.apal.2022.103212174:3(103212)Online publication date: Mar-2023
https://doi.org/10.1016/j.apal.2022.103212
Diaconescu R(2022)The Axiomatic Approach to Non-Classical Model TheoryMathematics10.3390/math1019342810:19(3428)Online publication date: 21-Sep-2022
https://doi.org/10.3390/math10193428
Diaconescu R(2022)Representing 3/2-Institutions as Stratified InstitutionsMathematics10.3390/math1009150710:9(1507)Online publication date: 1-May-2022
https://doi.org/10.3390/math10091507
Diaconescu R(2022)Decompositions of stratified institutionsJournal of Logic and Computation10.1093/logcom/exac05433:7(1625-1664)Online publication date: 25-Aug-2022
https://doi.org/10.1093/logcom/exac054
Futatsugi K(2022)Advances of proof scores in CafeOBJScience of Computer Programming10.1016/j.scico.2022.102893224:COnline publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102893
Găină DKowalski T(2021)Lindström’s theorem, both syntax and semantics freeJournal of Logic and Computation10.1093/logcom/exab07332:5(942-975)Online publication date: 13-Dec-2021
https://doi.org/10.1093/logcom/exab073
Leuştean IMoangă NŞerbănuţă T(2021)Many-sorted hybrid modal languagesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2021.100644120(100644)Online publication date: Apr-2021
https://doi.org/10.1016/j.jlamp.2021.100644
Găină DKowalski T(2020)Fraïssé–Hintikka theorem in institutionsJournal of Logic and Computation10.1093/logcom/exaa042Online publication date: 3-Sep-2020
https://doi.org/10.1093/logcom/exaa042
Găină DNakamura MOgata KFutatsugi K(2020)Stability of termination and sufficient-completeness under pushouts via amalgamationTheoretical Computer Science10.1016/j.tcs.2020.09.024848(82-105)Online publication date: Dec-2020
https://doi.org/10.1016/j.tcs.2020.09.024

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Issue’s Table of Contents