V
i j k

Abstract

algebraic

annotations

1 Introduction

2 Annotations and Propositions

A Framework for Resource Monitoring and

Control

David A. Wright

Department of Computer Science

University of Tasmania

GPO Box 252C

Hobart 7001

[email protected]

October 31, 1995

In this paper a logical framework is proposed for intensional logics. The key feature of the proposal is the use of an annotated logic in which the annotations have an structure. This enables many features of intensional logics to be expressed in a modular way. Intensional logics speci ed in the framework generally have the same underlying logic with di erences between them restricted to the algebraic properties of the annotations and to certain permeability" predicates.

In this short paper I will outline a framework for intensional logics which uses annotations with algebraic structure to seperate the intensional aspects of the logic from the conventional aspects of the logic. I will then give three examples to illustrate the power of the framework. The examples capture two quite di erent kinds of intensional logic. For the second kind of logic (binding-time) a related logic is also developed to which demonstrates the utility of the framework for comparing similiar logics.

For each logic speci ed in the framework a key step is to specify an algebraic structure of . For the purposes of the logics of this paper we will employ, minimally, algebras containing addition and multiplication and two basic meta-values and 1 such that both operations are re exive, commutative, transitive and associative, and we shall require that multiplication be idempotent. will be the identity for addition and 1 will be the identity for multiplication. will be a zero element for multiplication. Variables may be (optionally) included in the algebra (as in [5]). The set of variables will be denoted by . Meta-variables for annotations are denoted , , , . . . .