Abstract
Since its introduction by Goguen and Burstall in 1984, the theory of institutions has been one of the most widely accepted formalizations of abstract model theory. This work was extended by a number of researchers, José Meseguer among them, who presented General Logics, an abstract framework that complements the model theoretical view of institutions by defining the categorical structures that provide a proof theory for any given logic. In this paper we intend to complete this picture by providing the notion of Satisfiability Calculus, which might be thought of as the semantical counterpart of the notion of proof calculus, that provides the formal foundations for those proof systems that use model construction techniques to prove or disprove a given formula, thus “implementing” the satisfiability relation of an institution.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Goguen, J.A., Burstall, R.M.: Introducing institutions. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 221–256. Springer, Heidelberg (1984)
Meseguer, J.: General logics. In: Ebbinghaus, H.D., Fernandez-Prida, J., Garrido, M., Lascar, D., Artalejo, M.R. (eds.) Proceedings of the Logic Colloquium 1987, Granada, Spain, vol. 129, pp. 275–329. North Holland (1989)
Fiadeiro, J.L., Maibaum, T.S.E.: Generalising interpretations between theories in the context of π-institutions. In: Burn, G., Gay, D., Ryan, M. (eds.) Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods, London, UK, pp. 126–147. Springer (1993)
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)
Tarlecki, A.: Moving between logical systems. In: Haveraaen, M., Owe, O., Dahl, O.J. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)
Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76(2-3), 165–210 (1988)
Tarlecki, A.: Abstract specification theory: an overview. In: Broy, M., Pizka, M. (eds.) Proceedings of the NATO Advanced Study Institute on Models, Algebras and Logic of Engineering Software, Marktoberdorf, Germany. NATO Science Series, pp. 43–79. IOS Press (2003)
Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002)
Mossakowski, T., Tarlecki, A.: Heterogeneous logical environments for distributed specifications. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 266–289. Springer, Heidelberg (2009)
Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical Computer Science 285(2), 289–318 (2002)
Diaconescu, R.: Grothendieck institutions. Applied Categorical Structures 10(4), 383–402 (2002)
Diaconescu, R. (ed.): Institution-independent Model Theory. Studies in Universal Logic, vol. 2. Birkhäuser (2008)
Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)
Tarlecki, A.: Towards heterogeneous specifications. In: Gabbay, D., de Rijke, M. (eds.) Frontiers of Combining Systems. Studies in Logic and Computation, vol. 2, pp. 337–360. Research Studies Press (2000)
Cengarle, M.V., Knapp, A., Tarlecki, A., Wirsing, M.: A heterogeneous approach to UML semantics. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 383–402. Springer, Heidelberg (2008)
Beth, E.W.: The Foundations of Mathematics. North Holland (1959)
Beth, E.W.: Semantic entailment and formal derivability. In: Hintikka, J. (ed.) The Philosophy of Mathematics, pp. 9–41. Oxford University Press (1969) (reprinted from [34])
Herbrand, J.: Investigation in proof theory. In: Goldfarb, W.D. (ed.) Logical Writings, pp. 44–202. Harvard University Press (1969) (translated to English from [35])
Gentzen, G.: Investigation into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North Holland (1969) (translated to English from [36])
Smullyan, R.M.: First-order Logic. Dover Publishing (1995)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965)
McLane, S.: Categories for working mathematician. Graduate Texts in Mathematics. Springer, Berlin (1971)
Fiadeiro, J.L.: Categories for software engineering. Springer (2005)
Lopez Pombo, C.G., Castro, P., Aguirre, N.M., Maibaum, T.S.E.: Satisfiability calculus: the semantic counterpart of a proof calculus in general logics. Technical report, McMaster University, Centre for Software Certification (2011)
Fitting, M.: Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic 13(2), 237–247 (1972) (Lehman College)
Goguen, J.A., Rosu, G.: Institution morphisms. Formal Asp. Comput. 13(3-5), 274–307 (2002)
Castro, P.F., Aguirre, N.M., López Pombo, C.G., Maibaum, T.S.E.: Towards managing dynamic reconfiguration of software systems in a categorical setting. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 306–321. Springer, Heidelberg (2010)
Castro, P.F., Aguirre, N., López Pombo, C.G., Maibaum, T.: A categorical approach to structuring and promoting Z specifications. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 73–91. Springer, Heidelberg (2013)
Blackburn, P., de Rijke, M., Venema, Y.: Modal logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001)
Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3), 427–443 (1997)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology 11(2), 256–290 (2002)
Moura, L.D., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Communications of the ACM 54(9), 69–77 (2011)
Beth, E.W.: Semantic entailment and formal derivability. Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde 18(13), 309–342 (1955) (reprinted in [17])
Herbrand, J.: Recherches sur la theorie de la demonstration. PhD thesis, Université de Paris (1930) (English translation in [18])
Gentzen, G.: Untersuchungen tiber das logische schliessen. Mathematische Zeitschrijt 39, 176–210, 405–431 (1935) (English translation in [19])
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
López Pombo, C.G., Castro, P.F., Aguirre, N.M., Maibaum, T.S.E. (2013). Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics. In: Martí-Oliet, N., Palomino, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2012. Lecture Notes in Computer Science, vol 7841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37635-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-37635-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37634-4
Online ISBN: 978-3-642-37635-1
eBook Packages: Computer ScienceComputer Science (R0)