INVESTIGADORES
LOPEZ POMBO Carlos Gustavo
artículos
Título:
Satisfiability Calculi: the semantic counterpart of a proof calculus in general logics
Autor/es:
LOPEZ POMBO, CARLOS GUSTAVO; CASTRO, PABLO; AGUIRRE, NAZARENO M.; MAIBAUM, THOMAS S.E.
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer-Verlag
Referencias:
Lugar: Berlin; Año: 2013 vol. 7841 p. 195 - 211
ISSN:
0302-9743
Resumen:
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. This work was extended by a number of
researchers, José Meseguer among them, who presented General Logics,
an abstract framework that complements the model theoretical view of
institutions by defining the categorical structures that provide a proof
theory for any given logic. In this paper we intend to complete this
picture by providing the notion of Satisfiability Calculus,
which might be thought of as the semantical counterpart of the notion
of proof calculus, that 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.