Mostrar el registro sencillo del ítem
dc.contributor.author
Lopez Pombo, Carlos Gustavo
dc.contributor.author
Castro, Pablo
dc.contributor.author
Aguirre, Nazareno M.
dc.contributor.author
Maibaum, Thomas S.E.
dc.date.available
2021-01-21T15:36:24Z
dc.date.issued
2019-04
dc.identifier.citation
Lopez Pombo, Carlos Gustavo; Castro, Pablo; Aguirre, Nazareno M.; Maibaum, Thomas S.E.; Satisfiability Calculus: An Abstract Formulation of Semantic Proof Systems; IOS Press; Fundamenta Informaticae; 166; 4; 4-2019; 297-347
dc.identifier.issn
0169-2968
dc.identifier.uri
http://hdl.handle.net/11336/123309
dc.description.abstract
The theory of institutions, introduced by Goguen and Burstall in 1984, can be thought of as an abstract formulation of model theory. This theory has been shown to be particularly useful in computer science, as a mathematical foundation for formal approaches to software construction. Institution theory was extended by a number of researchers, José 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 given logic. In other words, Meseguer introduced the notion of proof calculus as a formalisation of syntactical deduction, thus ?implementing? the entailment relation of a given logic. In this paper we 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 construction techniques to prove or disprove a given formula, thus ?implementing? the satisfiability relation of an institution. These kinds of semantic proof methods have gained a great amount of interest in computer science over the years, as they provide the basic means for many automated theorem proving techniques.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
IOS Press
dc.rights
info:eu-repo/semantics/openAccess
dc.rights.uri
https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.subject
Category theory
dc.subject
General logics
dc.subject
Institutions
dc.subject.classification
Ciencias de la Computación
dc.subject.classification
Ciencias de la Computación e Información
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
dc.title
Satisfiability Calculus: An Abstract Formulation of Semantic Proof Systems
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2020-11-18T17:32:09Z
dc.journal.volume
166
dc.journal.number
4
dc.journal.pagination
297-347
dc.journal.pais
Países Bajos
dc.journal.ciudad
Amsterdam
dc.description.fil
Fil: Lopez Pombo, Carlos Gustavo. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigación en Ciencias de la Computación. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Instituto de Investigación en Ciencias de la Computación; Argentina
dc.description.fil
Fil: Castro, Pablo. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas Fisicoquímicas y Naturales. Departamento de Computación; Argentina
dc.description.fil
Fil: Aguirre, Nazareno M.. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas Fisicoquímicas y Naturales. Departamento de Computación; Argentina
dc.description.fil
Fil: Maibaum, Thomas S.E.. Mc Master University; Canadá
dc.journal.title
Fundamenta Informaticae
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://content.iospress.com/articles/fundamenta-informaticae/fi1804
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.3233/FI-2016-0000
Archivos asociados