This paper introduces a non-standard semantics for a modal version of constructive KT for contextual (assumptions-based) veri cation. The modal fragment expresses veri ability under extensions of contexts, enjoying adapted validity and (weak) monotonocity properties depending on satisfaction of the contextual data. ? Postdoctoral Fellow of the Research Foundation - Flanders (FWO). A liated Senior Researcher IEG, Oxford and GPI, Hertfordshire (UK).
Modelling contexts is a crucial issue for knowledge representation and problem
solving tasks ([
Our constructive contextual semantics presents two novel aspects: the representation of veri cation processes under open (non reduced) assumptions, and their modelling in a contextual dynamics. These properties are given by interpreting necessity as veri ability in the empty context of assumptions preserved to all extensions, and possibility as restricted validity. When performing queries on ontologies, one wants the theory to deal with validity of varying contextual values: [x=Straight, y=3Km, z=NoObstacles :: Path, n::Nat] prop P = Veichle Time(P(x, y, z)) ==> Value :: n [x=Bordeaux :: Wine, Red :: Colour] prop x = Bordeaux ==> Red(x) :: Bool
This dynamics should be admitted both at the typing level (e.g. with type declaration City in place of W ine, resulting in a di erent output) and at the value level (e.g. with type value 30km in place of 3km, resulting in a di erent computation z). The main applications are knowledge processes with unveri ed information, programming under contextual veri cation and output correcteness in distributed and staged computation. 2
Knowledge with Local and Global Contexts The language Lint is the union of two fragments Lint = fLver; Linf g. Lver is a positive (intuitionistic) language for direct veri cation processes, built in a standard way from propositional variables P = fA; B; C; : : :g, the propositional constant >, propositional unary and binary connectives :; &; _; . Linf is an extension of the previous language with ? and modal operators ; , obtained by de ning the satisfaction relation in a context . A set of knowledge states K = fKi j i 2 Ig is a nitely enumerable collection of nite sets of evaluated (modal and non-modal) formulas from Lint; each state is decorated with indices I = fi; j; k; : : :g; V = fx1; x2; : : :g denotes a nite set of free variables.
A model M ver = fK; ; R; vg is normal model with an accessibility relation on ordered states Ki Ki 2 K on which monotonicity is preserved for valuating propositional letters by a standard function v. Contexts ; 0 are sets of valuation functions from V to contents in a knowledge state. The partial order holds for knowledge states on the basis of the relevant informational contexts, where the function de nes the extension of holding for a given Ki to 0 of Kj (Ki Kj ), with at least one new propositional content assumed in Kj i. Each value obtained in context can be seen as the parametric module of the new language, collected into a strucutred list. vMinf ; Ki A is read as: \A is veri ed in Ki on the basis of information " and is based on the function := V 7! K, such that veri es A 2 Kj i M ver(Kiji j2I) 2 :A. A model M inf = fK; ; R; vg, has R as a symmetric accessibility relation on K induced by and v.
An informational context is the dynamic structure of information which speci es the actual program (or theory) against which the knowledge state is valid. The additional two speci c clauses for modalities in this language interpret contextual dynamics: { vM ; Ki { vM ; Ki
A i for any function A i there is a function it holds Ki A; for which it holds Ki
A.
Monotonicity for Linf is expressed under contextual constraints: Lemma 1 (Contextual Monotonicity for Linf ). If Ki 0 >, then Kj 0 > and if Ki j= A then Kj j= 0 A. > and for all ,
Introducing the distinction between global and local assumptions (see [
De nition 1 (Global Context). For any context , the global context given by Sf A1; : : : ; Ang such that := x 7! Ai 2 . De nition 2 (Local Context). For any context , the local context is given by Sf A1; : : : ; An j = f ; gg and := x 7! Ai 2 and 9Ai such that The resulting system has a correspondingly formulated consequence relation: Ki A; Ki A i for some it holds AAi. Tfhoer celvaesrsyof ,miotdheolsldMsK(Liver[Linf ) is equivalent to that of contextual `CKT ; Theorem 1. The system CKT ; is sound and complete with respect to the union class M(Lver[Linf ); i.e. for every set of formulae and formula A, it holds A i either V A, or A, or A.