Satisfiability calculus: The semantic counterpart of a proof calculus in general logics

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 co...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Lopez Pombo, C.G., Castro, P.F., Aguirre, N.M., Maibaum, T.S.E.
Formato:	SER
Materias:	Abstract framework Abstract model theory Categorical structure Formal foundation Proof calculus Proof system Proof theory Satisfiability Algebra Formal logic Semantics Calculations
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_03029743_v7841LNCS_n_p195_LopezPombo
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_03029743_v7841LNCS_n_p195_LopezPombo
record_format	dspace
spelling	todo:paper_03029743_v7841LNCS_n_p195_LopezPombo2023-10-03T15:19:31Z Satisfiability calculus: The semantic counterpart of a proof calculus in general logics Lopez Pombo, C.G. Castro, P.F. Aguirre, N.M. Maibaum, T.S.E. Abstract framework Abstract model theory Categorical structure Formal foundation Proof calculus Proof system Proof theory Satisfiability Algebra Formal logic Semantics Calculations 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. © IFIP International Federation for Information Processing 2013. Fil:Lopez Pombo, C.G. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v7841LNCS_n_p195_LopezPombo
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Abstract framework Abstract model theory Categorical structure Formal foundation Proof calculus Proof system Proof theory Satisfiability Algebra Formal logic Semantics Calculations
spellingShingle	Abstract framework Abstract model theory Categorical structure Formal foundation Proof calculus Proof system Proof theory Satisfiability Algebra Formal logic Semantics Calculations Lopez Pombo, C.G. Castro, P.F. Aguirre, N.M. Maibaum, T.S.E. Satisfiability calculus: The semantic counterpart of a proof calculus in general logics
topic_facet	Abstract framework Abstract model theory Categorical structure Formal foundation Proof calculus Proof system Proof theory Satisfiability Algebra Formal logic Semantics Calculations
description	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. © IFIP International Federation for Information Processing 2013.
format	SER
author	Lopez Pombo, C.G. Castro, P.F. Aguirre, N.M. Maibaum, T.S.E.
author_facet	Lopez Pombo, C.G. Castro, P.F. Aguirre, N.M. Maibaum, T.S.E.
author_sort	Lopez Pombo, C.G.
title	Satisfiability calculus: The semantic counterpart of a proof calculus in general logics
title_short	Satisfiability calculus: The semantic counterpart of a proof calculus in general logics
title_full	Satisfiability calculus: The semantic counterpart of a proof calculus in general logics
title_fullStr	Satisfiability calculus: The semantic counterpart of a proof calculus in general logics
title_full_unstemmed	Satisfiability calculus: The semantic counterpart of a proof calculus in general logics
title_sort	satisfiability calculus: the semantic counterpart of a proof calculus in general logics
url	http://hdl.handle.net/20.500.12110/paper_03029743_v7841LNCS_n_p195_LopezPombo
work_keys_str_mv	AT lopezpombocg satisfiabilitycalculusthesemanticcounterpartofaproofcalculusingenerallogics AT castropf satisfiabilitycalculusthesemanticcounterpartofaproofcalculusingenerallogics AT aguirrenm satisfiabilitycalculusthesemanticcounterpartofaproofcalculusingenerallogics AT maibaumtse satisfiabilitycalculusthesemanticcounterpartofaproofcalculusingenerallogics
_version_	1807314415554396160

Satisfiability calculus: The semantic counterpart of a proof calculus in general logics

Ejemplares similares