{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:19:22Z","timestamp":1777645162709,"version":"3.51.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"4","license":[{"start":{"date-parts":[[2019,4,26]],"date-time":"2019-04-26T00:00:00Z","timestamp":1556236800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Fundamenta Informaticae"],"published-print":{"date-parts":[[2019,4,26]]},"abstract":"<jats:p>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\u00e9 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 \u201cimplementing\u201d 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\u2019s 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 \u201cimplementing\u201d 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.<\/jats:p>","DOI":"10.3233\/fi-2019-1804","type":"journal-article","created":{"date-parts":[[2019,4,26]],"date-time":"2019-04-26T11:43:03Z","timestamp":1556278983000},"page":"297-347","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["Satisfiability Calculus: An Abstract Formulation of Semantic Proof Systems"],"prefix":"10.1177","volume":"166","author":[{"given":"Carlos G.","family":"Lopez Pombo","sequence":"first","affiliation":[{"name":"CONICET-Universidad de Buenos Aires, Instituto de Investigaci\u00f3n en Ciencias de la Computaci\u00f3n (ICC), Argentina."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo F.","family":"Castro","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Universidad Nacional de R\u00edo Cuarto, R\u00edo Cuarto, Argentina."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nazareno M.","family":"Aguirre","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Universidad Nacional de R\u00edo Cuarto, R\u00edo Cuarto, Argentina."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas S.E.","family":"Maibaum","sequence":"additional","affiliation":[{"name":"Department of Computing & Software, McMaster University, Canada."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2019,4,26]]},"container-title":["Fundamenta Informaticae"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2019-1804","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2019-1804","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:31:30Z","timestamp":1777444290000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/FI-2019-1804"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,26]]},"references-count":0,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,4,26]]}},"alternative-id":["10.3233\/FI-2019-1804"],"URL":"https:\/\/doi.org\/10.3233\/fi-2019-1804","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4,26]]}}}