Affiliations: [a] CONICET-Universidad de Buenos Aires, Instituto de Investigación en Ciencias de la Computación (ICC), Argentina. clpombo@dc.uba.ar | [b] Department of Computer Science, Universidad Nacional de Río Cuarto, Río Cuarto, Argentina. pcastro@dc.exa.unrc.edu.ar | [c] Department of Computer Science, Universidad Nacional de Río Cuarto, Río Cuarto, Argentina. naguirre@dc.exa.unrc.edu.ar | [d] Department of Computing & Software, McMaster University, Canada. tom@maibaum.org
Correspondence:
[*]
Address for correspondence: Department of Computer Science, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina.
Note: [†] These authors are also members of the National Research Council of Argentina (CONICET).
Abstract: 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.
