Synchronization of Logics

Motivated by applications in software engineering, we propose two forms of combination of logics: synchronization on formulae and synchronization on models. We start by reviewing satisfaction systems, consequence systems, one-step derivation systems and theory spaces, as well as their functorial rel...

Full description

Saved in:
Bibliographic Details
Published in:Studia logica 1997-09, Vol.59 (2), p.217-247
Main Authors: Sernadas, Amílcar, Sernadas, Cristina, Caleiro, Carlos
Format: Article
Language:English
Subjects:
Category theory
Derivational morphology
Functors
Logical givens
Mathematical logic
Model theory
Morphisms
Reasoning
Signatures
Temporal logic
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Motivated by applications in software engineering, we propose two forms of combination of logics: synchronization on formulae and synchronization on models. We start by reviewing satisfaction systems, consequence systems, one-step derivation systems and theory spaces, as well as their functorial relationships. We define the synchronization on formulae of two consequence systems and provide a categorial characterization of the construction. For illustration we consider the synchronization of linear temporal logic and equational logic. We define the synchronization on models of two satisfaction systems and provide a categorial characterization of the construction. We illustrate the technique in two cases: linear temporal logic versus equational logic; and linear temporal logic versus branching temporal logic. Finally, we lift the synchronization on formulae to the category of logics over consequence systems.
ISSN:0039-3215
1572-8730
DOI:10.1023/A:1004904401346