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.
Type de document :
Communication dans un congrès
Narciso Martí-Oliet; Miguel Palomino. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. Springer, Lecture Notes in Computer Science, LNCS-7841, pp.195-211, 2013, Recent Trends in Algebraic Development Techniques. 〈10.1007/978-3-642-37635-1_12〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01485970
Contributeur : Hal Ifip <>
Soumis le : jeudi 9 mars 2017 - 15:33:25
Dernière modification le : jeudi 9 mars 2017 - 15:36:07
Document(s) archivé(s) le : samedi 10 juin 2017 - 14:34:14

Fichier

978-3-642-37635-1_12_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Carlos López Pombo, Pablo Castro, Nazareno Aguirre, Thomas Maibaum. Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics. Narciso Martí-Oliet; Miguel Palomino. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. Springer, Lecture Notes in Computer Science, LNCS-7841, pp.195-211, 2013, Recent Trends in Algebraic Development Techniques. 〈10.1007/978-3-642-37635-1_12〉. 〈hal-01485970〉

Partager

Métriques

Consultations de la notice

100

Téléchargements de fichiers

8