Studia Logica 59 (3):359-386 (1997)

Annotated logics were introduced by V.S. Subrahmanian as logical foundations for computer programming. One of the difficulties of these systems from the logical point of view is that they are not structural, i.e., their consequence relations are not closed under substitutions. In this paper we give systems of annotated logics that are equivalent to those of Subrahmanian in the sense that everything provable in one type of system has a translation that is provable in the other. Moreover these new systems are structural. We prove that these systems are weakly congruential, namely, they have an infinite system of congruence 1-formulas. Moreover, we prove that an annotated logic is algebraizable (i.e., it has a finite system of congruence formulas,) if and only if the lattice of annotation constants is finite.
Keywords Philosophy   Logic   Mathematical Logic and Foundations   Computational Linguistics
Categories (categorize this paper)
DOI 10.1023/A:1005036412368
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 63,417
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Correspondences Between Gentzen and Hilbert Systems.J. G. Raftery - 2006 - Journal of Symbolic Logic 71 (3):903 - 957.
XI Latin American Symposium on Mathematical Logic.Carlos Augusto Di Prisco - 1999 - Bulletin of Symbolic Logic 5 (4):495-524.

View all 7 citations / Add more citations

Similar books and articles


Added to PP index

Total views
35 ( #309,339 of 2,449,087 )

Recent downloads (6 months)
1 ( #442,577 of 2,449,087 )

How can I increase my downloads?


My notes