Background and Motivation

Modelling contexts is a crucial issue for knowledge representation and problem solving tasks ( [6]). The constructive treatment of contexts, interpreted as meaning determining environments in a pragmatic setting for indexical expressions ( [5]) or as databases for information retrieval, is characterized by the reduction of assumptions to verified instances. From a logical viewpoint, the formulation of a constructive contextual possible worlds semantics is an interesting challenge to pair the syntactic calculi presented in [2] for staged computation, in [9] for an operational semantics that quantifies over contexts and in [10] for a constructive type theory with refutable assumptions.

Our constructive contextual semantics presents two novel aspects: the representation of verification processes under open (non reduced) assumptions, and their modelling in a contextual dynamics. These properties are given by interpreting necessity as verifiability 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: This dynamics should be admitted both at the typing level (e.g. with type declaration City in place of W ine, resulting in a different output) and at the value level (e.g. with type value 30km in place of 3km, resulting in a different computation z). The main applications are knowledge processes with unverified information, programming under contextual verification and output correcteness in distributed and staged computation.

Knowledge with Local and Global Contexts

The language L int is the union of two fragments L int = {L ver , L inf }. L ver is a positive (intuitionistic) language for direct verification processes, built in a standard way from propositional variables P = {A, B, C, . . .}, the propositional constant , propositional unary and binary connectives ¬, &, ∨, ⊃. L inf is an extension of the previous language with ⊥ and modal operators , ♦, obtained by defining the satisfaction relation in a context Γ . A set of knowledge states K = {K i | i ∈ I} is a finitely enumerable collection of finite sets of evaluated (modal and non-modal) formulas from L int ; each state is decorated with indices I = {i, j, k, . . .}; V = {x 1 , x 2 , . . .} denotes a finite set of free variables.

A model M ver = {K, ≤, R, v} is normal model with an accessibility relation on ordered states K i ≤ K i ∈ K on which monotonicity is preserved for valuating propositional letters by a standard function v. Contexts Γ, Γ 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 γ defines the extension of Γ holding for a given K i to Γ of K j (K i ≤ γ K j ), with at least one new propositional content assumed in K j≥i . Each value obtained in context can be seen as the parametric module of the new language, collected into a strucutred list. v M inf , K i Γ A is read as: "A is verified in K i on the basis of information Γ " and is based on the function γ := V → K, such that γ verifies A ∈ K j iff M ver (K i|i≤j∈I ) ¬A. A model M inf = {K, ≤ γ , R, v}, has R as a symmetric accessibility relation on K induced by ≤ γ and v.

An informational context is the dynamic structure of information which specifies the actual program (or theory) against which the knowledge state is valid. The additional two specific clauses for modalities in this language interpret contextual dynamics:

-v M , K i Γ A iff for any function γ it holds K i Γ ≤γ A; -v M , K i Γ ♦A iff there is a function γ for which it holds K i Γ ≤γ A.

Monotonicity for L inf is expressed under contextual constraints:

Lemma 1 (Contextual Monotonicity for L inf ). If K i Γ and for all γ, Γ ≤ γ Γ , then K j Γ and if K i |= Γ A then K j |= Γ A.

Introducing the distinction between global and local assumptions (see [4]) allows to reduce derivability and consequence relations of the two procols to a unified frame.

Definition 1 (Global Context). For any context Γ , the global context Γ is given by{ A 1 , . . . , A n } such that γ := x → A i ∈ Γ . Definition 2 (Local Context). For any context Γ , the local context ♦Γ is given by {•A 1 , . . . , •A n | • = { , ♦}} and γ := x → A i ∈ Γ and ∃A i such that ♦A i .

The resulting system has a correspondingly formulated consequence relation: K i Γ A iff for every γ, it holds K i Γ ≤γ A; K i ♦Γ A iff for some γ it holds K i Γ ≤γ A. The class of models M (L ver ∪L inf ) is equivalent to that of contextual KT (see [1], [3], [7]) with and ♦: Theorem 1. The system CKT ,♦ is sound and complete with respect to the union class M (L ver ∪L inf ) ; i.e. for every set of formulae Γ and formula A, it holds Γ CKT ,♦ A iff either Γ ⊃ A, or Γ A, or ♦Γ A.