Talk "Satisfiability calculus: the semantic counterpart of a proof calculus in general logics"

by Carlos Gustavo Lopez Pombo

Sat, 16 March 2013 at 02:30 pm in Rome, Italy

Joint work with: Tomas S.E. Maibaum, Pablo Castro, Nazareno Aguirre, Paula Chocrón

Abstract: Since its introduction by Goguen and Burstall in 1984, the theory of Institutions has been one of the most widely accepted formal- izations of abstract model theory. This work was extended by a number of researchers, Jos ́e Meseguer among them, who presented General Log- ics; 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 pic- ture 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.