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
Autor principal:	López Pombo, Carlos Gustavo
Publicado:	2013
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:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7841LNCS_n_p195_LopezPombo 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	paper:paper_03029743_v7841LNCS_n_p195_LopezPombo
record_format	dspace
spelling	paper:paper_03029743_v7841LNCS_n_p195_LopezPombo2023-06-08T15:28:49Z Satisfiability calculus: The semantic counterpart of a proof calculus in general logics López Pombo, Carlos Gustavo 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. 2013 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7841LNCS_n_p195_LopezPombo 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 López Pombo, Carlos Gustavo 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.
author	López Pombo, Carlos Gustavo
author_facet	López Pombo, Carlos Gustavo
author_sort	López Pombo, Carlos Gustavo
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
publishDate	2013
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7841LNCS_n_p195_LopezPombo http://hdl.handle.net/20.500.12110/paper_03029743_v7841LNCS_n_p195_LopezPombo
work_keys_str_mv	AT lopezpombocarlosgustavo satisfiabilitycalculusthesemanticcounterpartofaproofcalculusingenerallogics
_version_	1768544409189613568

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

Ejemplares similares