A Constructive Modal Semantics for Contextual Verification Giuseppe Primiero? Centre for Logic and Philosophy of Science University of Ghent (Belgium) Blandijnberg 2, room 231, 9000 Gent Giuseppe.Primiero@UGent.be Abstract. This paper introduces a non-standard semantics for a modal version of constructive KT for contextual (assumptions-based) verifi- cation. The modal fragment expresses verifiability under extensions of contexts, enjoying adapted validity and (weak) monotonocity properties depending on satisfaction of the contextual data. 1 Background and Motivation Modelling contexts is a crucial issue for knowledge representation and problem solving tasks ([6]). The constructive treatment of contexts, interpreted as mean- ing 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 repre- sentation of verification processes under open (non reduced) assumptions, and their modelling in a contextual dynamics. These properties are given by inter- preting 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: [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 ? Postdoctoral Fellow of the Research Foundation - Flanders (FWO). Affiliated Senior Researcher IEG, Oxford and GPI, Hertfordshire (UK). This dynamics should be admitted both at the typing level (e.g. with type dec- laration 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 compu- tation z). The main applications are knowledge processes with unverified infor- mation, programming under contextual verification 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 = {Lver , Linf }. Lver 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 ¬, &, ∨, ⊃. Linf 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 = {Ki | i ∈ I} is a finitely enumerable collection of finite sets of evaluated (modal and non-modal) formulas from Lint ; each state is decorated with indices I = {i, j, k, . . .}; V = {x1 , x2 , . . .} denotes a finite set of free variables. A model M ver = {K, ≤, R, v} is normal model with an accessibility relation on ordered states Ki ≤ Ki ∈ 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 γ defines 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. vM inf , Ki Γ A is read as: “A is verified in Ki on the basis of information Γ ” and is based on the function γ := V 7→ K, such that γ verifies A ∈ Kj iff M ver (Ki|i≤j∈I ) 2 ¬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 spec- ifies the actual program (or theory) against which the knowledge state is valid. The additional two specific clauses for modalities in this language interpret con- textual dynamics: – vM , Ki Γ A iff for any function γ it holds Ki Γ ≤γ A; – vM , Ki Γ ♦A iff there is a function γ for which it holds Ki Γ ≤γ A. Monotonicity for Linf is expressed under contextual constraints: Lemma 1 (Contextual Monotonicity for Linf ). If Ki Γ > and for all γ, 0 0 Γ ≤γ Γ 0  >, then Kj Γ > and if Ki |=Γ A then Kj |=Γ 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 S 1 (Global Context). For any context Γ , the global context Γ is given by {A1 , . . . , An } such that γ := x 7→ Ai ∈ Γ . Definition S 2 (Local Context). For any context Γ , the local context ♦Γ is given by {◦A1 , . . . , ◦An | ◦ = {, ♦}} and γ := x 7→ Ai ∈ Γ and ∃Ai such that ♦Ai . The resulting system has a correspondingly formulated consequence relation: Ki Γ A iff for every γ, it holds Ki Γ ≤γ A; Ki ♦Γ A iff for some γ it holds ver inf Ki Γ ≤γ A. The class of models M(L ∪L ) 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 ver inf union class M(L ∪L ) ; i.e. V for every set of formulae Γ and formula A, it holds Γ `CKT,♦ A iff either  Γ ⊃ A, or Γ A, or ♦Γ A. References 1. Alechina, N. Mendler, M., de Paiva, V., Ritter, E., “Categorical and Kripke Se- mantics for Constructive S4 Modal Logic”, Proceedings 15th Int. Workshop on Computer Science Logic, CSL’01, Paris, France, 10–13 Sept. 2001, pp. 292–307, Springer-Verlag, 2001. 2. Davies, R., Pfenning, F., “A modal Analysis of Staged Computation”, Journal of the ACM, vol.48, n.3, pp.555-604. 3. de Paiva, V., “Natural deduction and context as (constructive) modality”, in Pro- ceedings of the 4th International and Interdisciplinary Conference - CONTEXT03, Stanford, vol. 2680 of Lecture Notes in Artificial Intelligence, Springer Verlag, 2003. 4. Fitting, M., Basic Modal Logic, in D.M. Gabbay, C.J. Hogger, J.A. Robinson (eds), Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 4, 368– 449, Oxford University Press, 1994. 5. Giunchiglia, F., Bouquet, F., “Introduction to contextual reasoning. An Artificial Intelligence perspective”, in: B. Kokinov (ed.), Perspectives on Cognitive Science, vol. 3, NBU Press, Sofia, 1997, pp. 138-159. 6. McCarthy, J., “Notes on formalizing context”, in Proceedings of the 13th Joint Conference on Artificial Intelligence (IJCAI-93), 1993. 7. Mendler, M., de Paiva, V., “Constructive CK for Contexts”, in Proceedings of the first Workshop on Context Representation and Reasoning - CONTEXT05, Stan- ford, 2005. 8. Nanevski, A., Pfenning, F., Pientka, B., “Contextual Modal Type Theory”, in ACM Transactions on Computational Logic, vol. 9(3), pp.1-48, 2008. 9. Pientka, B., Dunfield, J., “Programming with Proofs and Explicit Contexts”, Pro- ceedings of the 10th international ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Valencia, SPain, ACM, pp.163-173. 10. Primiero, G., “Constructive contextual modal judgments for rea- soning from open assumptions”, Technical Report 542, Cen- tre for Logic and Philosophy of Science, Ghent University, 2009; http://logica.ugent.be/centrum/preprints/primiero open assumptions.pdf.