Satisfiability Calculus: An Abstract Formulation of Semantic Proof Systems

CARLOS LOPEZ POMBO; PABLO F. CASTRO; NAZARENO AGUIRRE; T.S.E. MAIBAUM

FUNDAMENTA INFORMATICAE

IOS PRESS

Lugar: Amsterdam; Año: 2019 vol. 166 p. 297 - 347

0169-2968

The theory of institutions, introduced by Goguen and Burstall in 1984, can be thoughtof as an abstract formulation of model theory. This theory has been shown to be particularlyuseful in computer science, as a mathematical foundation for formal approaches to software construction. Institution theory was extended by a number of researchers, Jose 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 givenlogic. In other words, Meseguer introduced the notion of proof calculus as a formalisation ofsyntactical deduction, thus ?implementing? the entailment relation of a given logic. In this paperwe 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 constructiontechniques to prove or disprove a given formula, thus ?implementing? the satisfiability relationof an institution. These kinds of semantic proof methods have gained a great amount of interestin computer science over the years, as they provide the basic means for many automated theoremproving techniques.