Satisfiability Calculus : An Abstract Formulation of Semantic Proof Systems

• Autorzy: Lopez Pombo Carlos G. , Castro Pablo F. , Aguirre Nazareno M. , Maibaum Thomas S. E.

Identyfikatory

DOI

10.3233/FI-2019-1804

• Języki publikacji: EN

Abstrakty

EN

The theory of institutions, introduced by Goguen and Burstall in 1984, can be thought of as an abstract formulation of model theory. This theory has been shown to be particularly useful in computer science, as a mathematical foundation for formal approaches to software construction. Institution theory was extended by a number of researchers, José Meseguer among them, who, in 1989, presented General Logics , wherein the model theoretical view of institutions is complemented by providing (categorical) structures supporting the proof theory of any given logic. In other words, Meseguer introduced the notion of proof calculus as a formalisation of syntactical deduction, thus “implementing” the entailment relation of a given logic. In this paper we follow the approach initiated by Goguen and introduce the concept of Satisfiability Calculus. This concept can be regarded as the semantical counterpart of Meseguer’s notion of proof calculus, as it provides the formal foundations for those proof systems that resort to model construction techniques to prove or disprove a given formula, thus “implementing” the satisfiability relation of an institution. These kinds of semantic proof methods have gained a great amount of interest in computer science over the years, as they provide the basic means for many automated theorem proving techniques.

Słowa kluczowe

EN

formal methods; institution theory; semantic proof systems

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 166, nr 4
• Strony: 297--347
• Opis fizyczny: Bibliogr. 75 poz., rys.

Twórcy

autor

Lopez Pombo Carlos G.

• CONICET-Universidad de Buenos Aires, Instituto de Investigación en Ciencias de la Computación (ICC), Argentina

autor

Castro Pablo F.

• Department of Computer Science, Universidad Nacional de Río Cuarto, Río Cuarto, Argentina

autor

Aguirre Nazareno M.

• Department of Computer Science, Universidad Nacional de Río Cuarto, Río Cuarto, Argentina

autor

Maibaum Thomas S. E.

• Department of Computing & Software, McMaster University, Canada

Bibliografia

• [1] Goguen JA, Burstall RM. Introducing Institutions. In: Clarke EM, Kozen D (eds.), Proceedings of the Carnegie Mellon Workshop on Logic of Programs, volume 184 of Lecture Notes in Computer Science. Springer-Verlag, 1984 pp. 221-256. doi:10.1007/3-540-12896-4_366.
• [2] Meseguer J. General logics. In: Ebbinghaus HD, Fernandez-Prida J, Garrido M, Lascar D, Artalejo MR (eds.), Proceedings of the Logic Colloquium ’87, volume 129. North Holland, Granada, Spain, 1989 pp.275-329.
• [3] Fiadeiro JL, Maibaum TSE. 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. Springer-Verlag, London, UK, 1993 pp. 126-147.doi:10.1007/978-1-4471-3503-6_10.
• [4] Goguen JA, Burstall RM. Institutions: abstract model theory for specification and programming. Journal of the ACM, 1992; 39(1):95-146. doi:10.1145/147508.147524.
• [5] Tarlecki A. Moving between logical systems. In: Haveraaen M, Owe O, Dahl OJ (eds.), Selected papers from the 11th Workshop on Specification of Abstract Data Types Joint with the 8th COMPASS Workshop on Recent Trends in Data Type Specification, volume 1130 of Lecture Notes in Computer Science. Springer-Verlag, 1996 pp. 478-502. doi:10.1007/3-540-61629-2_59.
• [6] Goguen JA, Roşu G. Institution Morphisms. Formal Aspects of Computing, 2002; 13(3-5):274-307. doi:10.1007/s001650200013.
• [7] Sannella D, Tarlecki A. Specifications in an arbitrary institution. Information and computation, 1988; 76(2-3):165-210. URL https://doi.org/10.1016/0890-5401(88)90008-9.
• [8] Sannella D, Tarlecki A. Toward Formal Development of Programs from Algebraic Specifications: Implementations Revisited. Acta Informatica, 1988; 25(3):233-281. See also [71]. doi:10.1007/BF00283329.
• [9] Mossakowski T. Heterogeneous Development Graphs and Heterogeneous Borrowing. In: Nielsen M, Engberg U (eds.), Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science. Springer-Verlag, London, UK, 2002 pp.326-341. doi:10.1007/3-540-45931-6_23.
• [10] Mossakowski T, Tarlecki A. Heterogeneous Logical Environments for Distributed Specifications. In: Corradini A, Montanari U (eds.), Proceedings of 19th International Workshop in Algebraic Development Techniques, volume 5486 of Lecture Notes in Computer Science. Springer-Verlag, Pisa, Italy, 2009 pp.266-289. doi:10.1007/978-3-642-03429-9_18.
• [11] Diaconescu R, Futatsugi K. Logical foundations of CafeOBJ. Theoretical Computer Science, 2002; 285(2):289-318. URL https://doi.org/10.1016/S0304-3975(01)00361-9.
• [12] Diaconescu R. Grothendieck institutions. Applied Categorical Structures, 2002; 10(4):383-402. doi:10.1023/A:1016330812768.
• [13] Diaconescu R (ed.). Institution-independent Model Theory, volume 2 of Studies in Universal Logic. Birkhäuser, 2008. ISBN-13:978-3764387075, 10:3764387076.
• [14] Mossakowski T, Maeder C, Luttich K. The heterogeneous tool set, Hets. In: Grumberg O, Huth M (eds.), Proceedings of the 13th. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), volume 4424 of Lecture Notes in Computer Science. Springer-Verlag, Braga, Portugal, 2007 pp. 519-522. doi:10.1007/978-3-540-71209-1_40.
• [15] Tarlecki A. Towards heterogeneous specifications. In: Gabbay D, de Rijke M (eds.), Frontiers of Combining Systems, volume 2 of Studies in Logic and Computation, pp. 337-360. Research Studies Press, 2000.
• [16] Cengarle MV, Knapp A, Tarlecki A, Wirsing M. A heterogeneous approach to UML semantics. In: Degano P, DeNicola R, Meseguer J (eds.), Proceedings of Concurrency, graphs and models (Essays dedicated to Ugo Montanari on the occasion of his 65th. birthday), number 5065 in Lecture Notes in Computer Science. Springer-Verlag, Edinburgh, Scotland, 2008 pp. 383-402. doi:10.1007/978-3-540-68679-8_23.
• [17] Beth EW. The Foundations of Mathematics. North Holland, 1959. ASIN: B0006EUQIQ.
• [18] Beth EW. Semantic entailment and formal derivability. In: Hintikka J (ed.), The Philosophy of Mathematics, pp. 9-41. Oxford University Press, 1969. Reprinted from [72].
• [19] Herbrand J. Investigation in Proof Theory. In: Goldfarb WD (ed.), Logical Writings, pp. 44-202. Harvard University Press, 1969. Translated to english from [73].
• [20] Gentzen G. Investigation into logical deduction. In: Szabo ME (ed.), The Collected Papers of Gerhard Gentzen, pp. 68-131. North Holland, 1969. Translated to english from [74].
• [21] Smullyan RM. First-order Logic. Dover Publishing, 1995. ISBN-10:0486683702, 13:978-0486683706.
• [22] Robinson JA. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 1965; 12(1):23-41. doi:10.1145/321250.321253.
• [23] Emerson EA. Temporal and Modal Logic. In: van Leeuwen J (ed.), Handbook of Theoretical Computer Science, volume B, pp. 995-1072. Elsevier, Amsterdam, 1990. URL https://doi.org/10.1016/B978-0-444-88074-1.50021-4.
• [24] Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, New York, NY, USA, 1992. ISBN:0-387-97664-7.
• [25] Emerson EA, Clarke EM. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 1982; 2(3):241-266. URL https://doi.org/10.1016/0167-6423(83)90017-5.
• [26] Attie PC. Synthesis of large dynamic concurrent programs from dynamic specifications. Formal Methods in System Design, 2016; 48(1-2):94-147. doi:10.1007/s10703-016-0252-9.
• [27] Degiovanni R, Ricci N, Alrajeh D, Castro P, Aguirre NM. Goal-conflict Detection Based on Temporal Satisfiability Checking. In: Lo D, Apel S, Khurshid S (eds.), Proceedings of 31st IEEE/ACM International Conference on Automated Software Engineering. ACM Press, New York, NY, USA, 2016 pp. 507-518. doi:10.1145/2970276.2970349.
• [28] Lopez Pombo CG, Castro P, Aguirre NM, Maibaum TSE. Satisfiability calculi: the semantic counterpart of proof calculi in general logics. In: Martí-Oliet N, Palomino Tarjuelo M(eds.), Proceedings of 21st International Workshop on Algebraic Development Techniques (WADT 2012) and IFIP International Federation for Information Processing (2013), volume 7841 of Lecture Notes in Computer Science. Springer-Verlag, Salamanca, Spain, 2013 pp. 195-211. doi:10.1007/978-3-642-37635-1_12.
• [29] McLane S. Categories for working mathematician. Graduate Texts in Mathematics. Springer-Verlag, Berlin, Germany, 1971.
• [30] Fiadeiro JL. Categories for software engineering. Springer-Verlag, 2005. ISBN:3540209093.
• [31] Cassano V, Lopez Pombo CG, Maibaum TSE. Entailment Systems for Default Reasoning. In: Martí-Oliet N, Palomino Tarjuelo M (eds.), Proceedings of 21st International Workshop on Algebraic Development Techniques (WADT 2012). Salamanca, Spain, 2012 pp. 28-30.
• [32] Reiter R. A Logic for Default Reasoning. Artificial Intelligence, 1980; 13(1-2):81-132. URL https://doi.org/10.1016/0004-3702(80)90014-4.
• [33] Tarlecki A. Bits and pieces of the theory of institutions. In: Pitt DH, Abramsky S, Poigné A, Rydeheard DE (eds.), Proceedings of the Category Theory and Computer Programming, tutorial and workshop, volume 240 of Lecture Notes in Computer Science. Springer-Verlag, 1986 pp. 334-363. doi:10.1007/3-540-17162-2_132.
• [34] Lopez Pombo CG. Fork algebras as a tool for reasoning across heterogeneous specifications. Ph.D. thesis, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, 2007. Promotor: Marcelo F. Frias.
• [35] Frias MF, Baum GA, Maibaum TSE. Interpretability of first-order dynamic logic in a relational calculus. In: de Swart H (ed.), Proceedings of the 6th. Conference on Relational Methods in Computer Science (RelMiCS) - TARSKI, volume 2561 of Lecture Notes in Computer Science. Springer-Verlag, Oisterwijk, The Netherlands, 2002 pp. 66-80. doi:10.1007/3-540-36280-0_5.
• [36] Haeberer AM, Veloso PA. Partial relations for program derivation: adequacy, inevitability and expressiveness. In: Proceedings of IFIP TC2 working conference on constructing programs from specifications. IFIP TC2: Software: Theory and Practice, North Holland, 1991 pp. 310-352.
• [37] Frias MF. Fork algebras in algebra, logic and computer science, volume 2 of Advances in logic. World Scientific Publishing Co., Singapore, 2002. ISBN-10:9810248768, 13:978-9810248765.
• [38] Fitting M. Tableau Methods of Proof for Modal Logics. Lehman College. Notre Dame Journal of Formal Logic, 1972; 13(2):237-247. doi:10.1305/ndjfl/1093894722.
• [39] Lewis CI. The Place of Intuition in Knowledge. Ph.D. thesis, Harvard University, 1910. Advisor: Tomas S. E. Maibaum.
• [40] Lewis CI, Langford CH. Symbolic logic. The Century Co., 1932.
• [41] Barcan RC. A Functional Calculus of First Order Based on Strict Implication. Journal of Symbolic Logic, 1946; 11(1):1-16. doi:10.2307/2269159.
• [42] Barcan RC. The Deduction Theorem in a Functional Calculus of First Order Based on Strict Implication. Journal of Symbolic Logic, 1946; 11(4):115-118. doi:10.2307/2268309.
• [43] Barcan RC. The Identity of Individuals in a Strict Functional Calculus of Second Order. Journal of Symbolic Logic, 1947; 12(1):12-15. doi:10.2307/2267171.
• [44] Kripke SA. Semantical Analysis of Modal Logic I. Normal Propositional Calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 1963; 9(56):67-96. URL https://doi.org/10.1002/malq.19630090502.
• [45] Kripke SA. Semantical considerations on modal logic. Acta Philosophica Fennica, 1963; 16:83-94.
• [46] Fitting M. First-Order Modal Tableaux. Journal of Automated Reasoning, 1988; 4(2):191-213. doi:10.1007/BF00244394.
• [47] Fitting M, Mendelsohn RL. First-Order Modal Logic, volume 277 of Synthese Library. Springer Netherlands, 1998. ISBN-10:0792353358, 13:978-0792353355.
• [48] Enderton HB. A mathematical introduction to logic. Academic Press, 1972.
• [49] Schoenfield JR. Degrees of unsolvability. Number 2 in Mathematical studies. North Holland, 1971. ISBN:9780080871134.
• [50] Fitting M. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese Library. Springer Netherlands, 1983. doi:10.1007/978-94-017-2794-5.
• [51] Lopez Pombo CG, Castro P, Aguirre NM, Maibaum TSE. A Heterogeneous Characterisation of Component-Based System Design in a Categorical Setting. In: Ciobanu G, Ipate F (eds.), Proceedings of 11th International Colloquium Theoretical Aspects of Computing - ICTAC 2014, volume 8687 of Lecture Notes in Computer Science. Springer-Verlag, 2014 pp. 314-332. doi:10.1007/978-3-319-10882-7_19.
• [52] Castro P, Aguirre NM, Lopez Pombo CG, Maibaum TSE. A Categorical Approach to Structuring and Promoting Z Specifications. In: Pasareanu CS, Salaün G (eds.), Proceedings of 9th International Symposium Formal Aspects of Component Software - FACS 2012, volume 7684 of Lecture Notes in Computer Science. Springer-Verlag, 2013 pp. 73-91. doi:10.1007/978-3-642-35861-6_5.
• [53] Castro P, Aguirre NM, Lopez Pombo CG, Maibaum TSE. Categorical foundations for structured specifications in Z. Formal Aspects of Computing, 2015; 27(5-6):831-865. doi:10.1007/s00165-015-0336-0.
• [54] Borzyszkowski T. Logical systems for structured specifications. Theoretical Computer Science, 2002; 286(2):197-245. URL https://doi.org/10.1016/S0304-3975(01)00317-6.
• [55] Mossakowski T, Tarlecki A. A Relatively Complete Calculus for Structured Heterogeneous Specifications. In: Muscholl A (ed.), Proceedings of 17th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2014), held as Part of the European Joint Conferences on Theory and Practice of Software, volume 8412 of Lecture Notes in Computer Science. Springer-Verlag, 2014 pp.441-456. doi:10.1007/978-3-642-54830-7_29.
• [56] Lopez Pombo CG, Frias MF. Chapter 16: (Heterogeneous) Structured Specifications in Logics Without Interpolation, volume 17 of Outstanding Contributions to Logic, chapter 16. Springer International publishing, 2018.
• [57] Castro P, Aguirre NM, Lopez Pombo CG, Maibaum TSE. Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting. In: Cavalcanti A, D’eharbe D, Gaudel MC, Woodcock J (eds.), Proceedings of Theoretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, volume 6255 of Lecture Notes in Computer Science. Springer-Verlag, Natal, Rio Grande do Norte, Brazil, 2010 pp. 306-321. doi:10.1007/978-3-642-14808-8_21.
• [58] Tarlecki A. Structural properties of some categories of institutions, 1998. Revised version of its original version of 1996.
• [59] Tarlecki A. Limits and colimits in some categories of institutions, 2006. Revised and extended version of [5]. doi:10.1007/BFb0084208.
• [60] Blackburn P, de Rijke M, Venema Y. Modal logic. Number 53 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. ISBN-13:978-0521527149, 10:0521527147.
• [61] Veloso PA, Haeberer AM, Frias MF. Fork algebras as algebras of logic. Abstracts of the Logic Colloquium ’94, 1995. p. 127. Also in [75].
• [62] Frias MF, Baum GA, Haeberer AM. Fork algebras in algebra, logic and computer science. Fundamenta Informaticae, 1997; 32:1-25.
• [63] Jónnson B, Tarski A. Boolean algebra with operators, part I. American Journal of Mathematics, 1951; 73:891-939.
• [64] Jónnson B, Tarski A. Boolean algebra with operators, part II. American Journal of Mathematics, 1952; 74:127-162.
• [65] Frias MF, Lopez Pombo CG. Interpretability of first-order linear temporal logics in fork algebras. Journal of Logic and Algebraic Programming, 2006; 66(2):161-184. URL https://doi.org/10.1016/j.jlap.2005.04.005.
• [66] Roşu G. Kan Extensions of Institutions. Journal of Universal Computer Science, 1999; 5(8):482-493. doi:10.3217/jucs-005-08-0482.
• [67] Kozen D. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 1997; 19(3):427-443. doi:10.1145/256167.256195.
• [68] Clavel M, Eker S, Lincoln P, Meseguer J. Principles of Maude. In: Meseguer J (ed.), Proceedings of the 1st. International Workshop on Rewriting Logic and its Applications (WRLA’96), volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996 pp. 65-89. URL https://doi.org/10.1016/S1571-0661(04)00034-9.
• [69] Jackson D. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology, 2002; 11(2):256-290. doi:10.1145/505145.505149.
• [70] de Moura LM, Bjørner N. Satisfiability modulo theories: introduction and applications. Communications of the ACM, 2011; 54(9):69-77. doi:10.1145/1995376.1995394.
• [71] Sannella D, Tarlecki A. Toward formal development of programs from algebraic specifications: implementations revisited. Technical Report 17, Laboratory for foundations of computer science, The University of Edinburgh, 1986. Preliminar version of [8].
• [72] Beth EW. Semantic entailment and formal derivability. Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde. Reprinted in [18]. 1955; 18(13):309-342. ASIN:B007F7P4T8.
• [73] Herbrand J. Recherches sur la theorie de la demonstration. Ph.D. thesis, Université de Paris, 1930. English translation in [19]. URL http://www.numdam.org/item?id=THESE_1930__110__1_0
• [74] Gentzen G. Untersuchungen tiber das logische Schliessen. English translation in [20]. Mathematische Zeitschrijt, 1935; 39:176-210 and 405-431. ISSN:0025-5874; 1432-1823.
• [75] Veloso PA, Haeberer AM, Frias MF. Fork algebras as algebras of logic. Bulletin of Symbolic Logic. 1995; 1(2):265-266. Also in [61].

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).