Skip to Main content Skip to Navigation
Conference papers

Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-01485970
Contributor : Hal Ifip <>
Submitted on : Thursday, March 9, 2017 - 3:33:25 PM
Last modification on : Wednesday, April 17, 2019 - 4:06:02 PM
Long-term archiving on: : Saturday, June 10, 2017 - 2:34:14 PM

File

978-3-642-37635-1_12_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Carlos López Pombo, Pablo Castro, Nazareno Aguirre, Thomas Maibaum. Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. pp.195-211, ⟨10.1007/978-3-642-37635-1_12⟩. ⟨hal-01485970⟩

Share

Metrics

Record views

554

Files downloads

390