Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics

Research Area: McSCert Reports Year: 2014
Type of Publication: Technical Report Keywords: Model theory, Satisfiability, Proof calculi, General logics
  • Carlos G. Lopez Pombo
  • Pablo F. Castro
  • Nazareno M. Aguirre
  • Thomas S. E. Maibaum
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; thus it has become the de facto foundation of any mathematical tool tailored to describe software artifacts. This work was extended by a number of researchers, José Meseguer among them, who, in 1989, presented General Logics; in this article he complements the model theoretical view of Institutions by defining (using the abstract language of Category Theory) the structures that provide a proof theory of any given logic. More concretely, he introduces the notion of proof calculus, which in some sense \implements" the deduction relation of an entailment system. In this paper we intend to complete the picture by providing the notion of Satisfiability Calculus, which might be thought of as the semantical counterpart of the notion of proof calculus, and 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.