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 applied to particular cases of hybrid logics with user-defined sharing, where the first-order variables in quantified sentences are interpreted uniformly across worlds.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Areces C, Blackburn P (2001) Bringing them all together. J Log Comput 11(5): 657–669
Astesiano E, Bidoit M, Kirchner H, Krieg-Brückner B, Mosses PD, Sannella D, Tarlecki A (2002) CASL: the Common Algebraic specification language. Theor Comput Sci 286(2): 153–196
Aiguier M, Diaconescu R (2007) Stratified institutions and elementary homomorphisms. Inf Process Lett 103(1): 5–13
Béziau J-Y (2006) 13 questions about universal logic. Bull Sect Log 35(2/3): 133–150
Béziau J-Y (2012) Universal logic: an anthology: from Paul Hertz to Dov Gabbay. Birkhäuser, Basel
Birkhoff G (1935) On the structure of abstract algebras. In: Mathematical proceedings of the Cambridge philosophical society, vol 31, pp 433–454,
Blackburn P (2000) Representation, reasoning, and relational structures: a hybrid logic manifesto. Log J IGPL 8(3): 339–365
Blackburn P, Marx M (2002) Tableaux for quantified hybrid logic. In: Egly U, Fermüller CG (eds) Automated reasoning with analytic tableaux and related methods, international conference, TABLEAUX 2002, Copenhagen, Denmark, July 30–August 1, 2002, proceedings, volume 2381 of lecture notes in computer science. Springer, pp 38–52
Braüner T (2011) Hybrid logic and its Proof-Theory, applied logic series, vol 37. Springer, Berlin
Carnielli W, Coniglio M, Gabbay DM, Gouveia P, Sernadas C (2008) Analysis and synthesis of logics—how To cut and paste reasoning systems. Applied logic series. Springer, Berlin
Codescu M, Găină D (2008) Birkhoff completeness in institutions. Log Univers 2(2): 277–309
Diaconescu R, Futatsugi K (2002) Logical foundations of CafeOBJ. Theor Comput Sci 285(2): 289–318
Diaconescu R (2003) Institution-independent ultraproducts. Fundam Inf 55(3-4): 321–348
Diaconescu R (2004) Herbrand theorems in arbitrary institutions. Inf Process Lett 90(1): 29–37
Diaconescu R (2006) Proof systems for institutional logic. J Log Comput 16(3): 339–357
Diaconescu R (2008) Institution-independent model theory. Studies in universal logic, 1 edn. Birkhäuser, Basel
Diaconescu R (2012) Borrowing interpolation. J Log Comput 22(3): 561–586
Diaconescu R (2016) Implicit kripke semantics and ultraproducts in stratified Institutions. J Log Comput. doi:10.1093/logcom/exw018
Diaconescu R (2016) Quasi-varieties and initial semantics for hybridized institutions. J Log Comput 26(3): 855–891
Diaconescu R, Madeira A (2016) Encoding hybridized institutions into first-order logic. Math Struct Comput Sci 26(5): 745–788
Finger M, Gabbay DM (1992) Adding a temporal dimension to a logic system. J Log Lang Inf 1(3): 203–233
Găină D, Futatsugi K, Ogata K (2012) Constructor-based logics.. J UCS 18(16): 2204–2233
Găină D, Petria M (2010) Completeness by forcing.. J Log Comput 20(6): 1165–1186
Găină D (2013) Interpolation in logics with constructors.. Theor Comput Sci 474: 46–59
Găină D (2015) Downward Löwenheim-Skolem theorem and interpolation in logics with constructors. J Log Comput. doi:10.1093/logcom/exv018
Găină D (2015) Foundations of logic programming in hybrid logics with user-defined sharing. TheoretComput Sci (submitted)
Găină D (2015) Foundations of logic programming in hybridised logics. In: Codescu M, Diaconescu R, Ţuţu I (eds) Recent trends in algebraic development techniques—22nd international workshop, WADT 2014, Sinaia, Romania, September 4–7, 2014, proceedings, volume 9463 of lecture notes in computer science. Springer, pp 69–89
Goguen J, Burstall R (1992) Institutions: abstract model theory for specification and programming. J Assoc Comput Mach 39(1): 95–146
Goguen J, Meseguer J (1985) Completeness of many-sorted equational logic. Houst J Math 11(3): 307–334
Goguen JA, Meseguer J (1992) Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor Comput Sci 105(2): 217–273
Goguen J (1994) Theorem proving and algebra. https://cseweb.ucsd.edu/~goguen/pubs/tp.html
Henkin L (1950) Completeness in the theory of types.. J Symb Log 15(2): 81–91
Madeira A (2013) Foundations and techniques for software reconfigurability. Ph.D. thesis, Universidades do Minho, Aveiro and Porto, Joint MAP-i Doctoral Programme
Meseguer J (1989) General logics. In: Ebbinghaus H-D, Fernandez-Prida J, Garrido M, Lascar D, Rodriguez Artalejo M (eds) Logic Colloquium ’87. Studies in logic and the foundations of mathematics, vol 129, North Holland, pp 275–329
Madeira A, Martins MA, Barbosa LS, Hennicker R (2015) Refinement in hybridised institutions.. Formal Asp Comput 27(2): 375–395
Martins MA, Madeira A, Diaconescu R, Barbosa LS (2011) Hybridization of institutions. In: Corradini A, Klin B, Cîrstea C (eds) Algebra and coalgebra in computer science—4th international conference, CALCO 2011, Winchester, UK, August 30—September 2, 2011, Proceedings, volume 6859 of lecture notes in computer science. Springer, pp 283–297
Neves R, Madeira A, Martins MA, Barbosa LS (2016) Proof theory for hybrid(ised) logics.. Sci Comput Program 126: 73–93
Passay S, Tinchev T (1991) An essay in combinatory dynamic logic.. Inf Comput 93(2): 263–332
Petria M (2007) An institutional version of Gödel’s completeness theorem. In: Mossakowski T, Montanari U, Haveraaen M (eds) Algebra and coalgebra in computer science, second international conference CALCO 2007, Bergen, Norway, August 20–24, 2007, proceedings, volume 4624 of lecture notes in computer science, Springer. pp 409–424
Prior A (1967) Past, present and future. Oxford books. OUP Oxford, Oxford
Schurz G (2011) Combinations and completeness transfer for quantified modal logics.. Log J IGPL 19(4): 598–616
Szepesia R, Ciocârlie H (2011) An overview on software reconfiguration.. Theory Appl Math Comput Sci 1(1): 74–79
Tarlecki A (1986) Bits and pieces of the theory of institutions. In: Pitt D, Abramsky S, Poigné A, Rydeheard D (eds) Proceedings, summer workshop on category theory and computer programming, lecture notes in computer science, vol 240. Springer, pp 334–360
Tarlecki A (1986) Quasi-varieties in abstract algebraic institutions.. J Comput Syst Sci 33(3): 333–360
Ţuţu I, Fiadeiro JL (2015) Revisiting the Institutional approach to Herbrand’s theorem. In: Moss LS, Sobocinski P (eds) 6th conference on Algebra and Coalgebra in computer science CALCO 2015, June 24–26, 2015, Nijmegen, The Netherlands, volume 35 of LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Wadern
Author information
Authors and Affiliations
Corresponding author
Additional information
Anne Haxthausen
Rights and permissions
About this article
Cite this article
Găină, D. Birkhoff style calculi for hybrid logics. Form Asp Comp 29, 805–832 (2017). https://doi.org/10.1007/s00165-016-0414-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-016-0414-y