Paper deep dive
TAPO-Description Logic for Information Behavior: Refined OBoxes, Inference, and Categorical Semantics
Takao Inoué
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 96%
Last extracted: 4/26/2026, 7:41:14 PM
Summary
The paper presents a refined version of TAPO-description logic (TAPO-DL) designed for analyzing information behavior. It moves beyond static knowledge representation by introducing a layered architecture: a static descriptive layer (TBox/ABox), a procedural layer (PBox) for branching and iteration, and a strengthened oracle-sensitive layer (OBox) for controlled external information import. The framework incorporates a metalevel guard-judgment layer to govern procedural transitions and provides a categorical semantics based on presheaves and sheaf-theoretic refinement. The model is illustrated through information-seeking behaviors like search and review-sensitive ordering.
Entities (9)
Relation Signals (5)
Takao Inoué → affiliatedwith → Yamato University
confidence 100% · Takao Inoué Faculty of Informatics, Yamato University, Osaka, Japan
TAPO-description logic → consistsof → TBox
confidence 100% · The framework is treated not as a single homogeneous object logic, but as a layered formalism consisting of a static descriptive layer (TBox/ABox), a procedural layer (PBox), and an oracle-sensitive layer (OBox).
TAPO-description logic → consistsof → PBox
confidence 100% · The framework is treated not as a single homogeneous object logic, but as a layered formalism consisting of a static descriptive layer (TBox/ABox), a procedural layer (PBox), and an oracle-sensitive layer (OBox).
TAPO-description logic → consistsof → OBox
confidence 100% · The framework is treated not as a single homogeneous object logic, but as a layered formalism consisting of a static descriptive layer (TBox/ABox), a procedural layer (PBox), and an oracle-sensitive layer (OBox).
TAPO-description logic → uses → Categorical Semantics
confidence 90% · We then give a categorical semantics for the resulting framework and indicate its sheaf-theoretic refinement.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:This paper develops a refined version of TAPO-description logic for the analysis of information behavior. The framework is treated not as a single homogeneous object logic, but as a layered formalism consisting of a static descriptive layer (TBox/ABox), a procedural layer (PBox), and an oracle-sensitive layer (OBox). To make this architecture mathematically explicit, we introduce a metalevel guard-judgment layer governing procedural branching and iteration. On this basis we formulate a core inference system for TAPO-description logic, covering static TBox/ABox reasoning, guarded procedural transition in the PBox, and validated external import in the OBox. We then give a categorical semantics for the resulting framework and indicate its sheaf-theoretic refinement. The theory is illustrated by examples of information-seeking behavior, including simple search behavior and review-sensitive ordering behavior in a curry restaurant. The aim is to treat not only static knowledge representation but also hesitation, external consultation, and action-guiding update within a unified logical setting.
Tags
Links
- Source: https://arxiv.org/abs/2604.21172v1
- Canonical: https://arxiv.org/abs/2604.21172v1
Trouble viewing inline? Open PDF directly →
Full Text
84,947 characters extracted from source content.
Expand or collapse full text
TAPO-Description Logic for Information Behavior: Refined OBoxes, Inference, and Categorical Semantics Takao Inoué Faculty of Informatics, Yamato University, Osaka, Japan inoue.takao@yamato-u.ac.jp (Date: April 22, 2026) Abstract. This paper develops a refined version of TAPO-description logic for the analysis of information behavior. The framework is treated not as a single homogeneous object logic, but as a layered formalism consisting of a static descriptive layer (TBox/ABox), a procedural layer (PBox), and an oracle-sensitive layer (OBox). To make this architecture mathematically explicit, we introduce a metalevel guard-judgment layer governing procedural branching and iteration. On this basis we formulate a core inference system for TAPO-description logic, covering static TBox/ABox reasoning, guarded procedural transition in the PBox, and validated external import in the OBox. We then give a categorical semantics for the resulting framework and indicate its sheaf-theoretic refinement. The theory is illustrated by examples of information-seeking behavior, including simple search behavior and review-sensitive ordering behavior in a curry restaurant. The aim is to treat not only static knowledge representation but also hesitation, external consultation, and action-guiding update within a unified logical setting. Key words and phrases: description logic, categorical semantics, TAPO-description logic, TBox, ABox, PBox, OBox, sheaf semantics, topos theory, knowledge representation 2020 Mathematics Subject Classification: 18F20, 03B70, 68T30, 18B25 Personal Email: takaoapple@gmail.com. I prefer my personal email address for correspondence. Contents 1 Introduction 2 Refined TAPO-description logic 2.1 Signature, concepts, and contexts 2.2 The TAPO architecture 2.3 Localization and restriction 3 The OBox as oracle interface and controlled external import 3.1 The strengthened OBox 3.2 Validated import 3.3 Restriction compatibility 3.4 Compositionality of oracle interfaces 3.5 Why the OBox is mathematically nontrivial 4 A core inference system for TAPO-description logic 4.1 Judgments 4.2 Static rules for the TBox and ABox 4.3 Guard judgments as a distinct layer 4.4 Transition rules for the PBox 4.5 Validated import rules for the OBox 4.6 Procedural invocation of the oracle layer 5 TAPO-structured knowledge objects 6 The TBox and ABox as categorical data 6.1 The TBox 6.2 The ABox 7 The PBox as a minimal imperative layer 7.1 Guards 7.2 Program syntax 7.3 Operational semantics and denotations 8 Sheaf-theoretic refinement 9 Soundness and the completeness problem 10 Information-behavior examples and discussion 10.1 Simple search behavior 10.2 Review-sensitive ordering behavior in a curry restaurant 11 Further directions References A TAPO-Description Logic as a Formal Analytic Layer for Browsing Theory A.1 Why Chang-style browsing is relevant here A.2 A TAPO reinterpretation of multidimensional browsing A.3 Formal decomposition of browsing dimensions A.4 A generic browsing episode in TAPO form A.5 Why this goes beyond a descriptive restatement A.6 Relation to interface-sensitive browsing A.7 Toward a formal research program 1. Introduction Description logic has long provided a mathematically precise language for structured knowledge representation. Its classical architecture is centered around a terminological component and an assertional component, usually called the TBox and the ABox. This framework has proved powerful for ontology engineering and semantic technologies, but many actual information environments involve more than static concepts and assertions. They also involve procedures, controlled update, and access to information obtained from outside the current knowledge state. The author previously introduced TAPO-description logic as a four-layered extension of the standard picture, consisting of a TBox, an ABox, a PBox, and an OBox [6]. In that earlier paper, the emphasis was on the conceptual motivation for enriching description logic by procedural and oracle-based components. The purpose of the present paper is to push that program in a more explicitly mathematical direction. In particular, we aim to isolate a clean inferential skeleton that is robust enough to support later categorical, sheaf-theoretic, and topos-theoretic refinement. Recent work has shown that ordinary description logics, especially systems around ℒALC and general TBoxes, admit meaningful category-theoretic semantics [7, 2, 8]. There are also broader categorical approaches to knowledge representation that lie close to description logic, for example the bicategorical relational framework of Patterson [11]. On a different but related side, recent NLP-oriented work on extracting formal models from natural-language specifications has made explicit the importance of conditional and action-oriented intermediate structure [5]. These developments suggest that the passage from set-theoretic semantics to structural semantics is natural and fruitful. Nevertheless, most direct semantics for description logic still concentrate on the static TBox/ABox core, while parsing-oriented approaches do not by themselves provide an intrinsic treatment of procedural knowledge. The present paper is intended as a next step: not a survey of those directions, but a categorical and proof-theoretic continuation of the TAPO program. From the viewpoint of information behavior, an additional nearby motivation comes from the literature on browsing. Chang and Rice treat browsing not as a weak substitute for directed search, but as a multidimensional and context-sensitive information activity shaped by motivation, interface structure, cognitive state, and available resources [4]. Related work by Chang emphasizes that browsing interfaces and patterns of information organization can materially influence subsequent user action [3], while the broader study of access and browsing by Rice, McCreadie, and Chang argues that observable query–answer episodes are often only one visible portion of a larger chain of informational activity [10]. This perspective is strongly compatible with the passage from TBox/ABox-structured to TAPO-structured description logic: once browsing, hesitation, reformulation, and externally mediated confirmation are taken seriously, procedural and oracle-sensitive layers cease to be optional embellishments and become mathematically natural components of the theory. The central thesis of the present paper is that these additional layers should be treated as genuine mathematical structure. The PBox should not be reduced to an informal programming metaphor; it should be represented by programs, guarded evaluations, and composable state transformations over localized knowledge states. Likewise, the OBox should not remain a vague placeholder for “external input.” It should be strengthened into a controlled interface equipped with admissible queries, contextual responses, compatibility with restriction, and explicit criteria for trusted and certified import. This strengthening of the OBox, together with the introduction of an explicit inferential layer for procedural control, is one of the main ways in which the present paper goes beyond the original formulation in [6]. A point that is essential for the present paper is that TAPO-DL should not be read as a single homogeneous object language. Rather, it is a layered formalism. The TBox and ABox form the static descriptive layer; the PBox provides a procedural layer with constructs such as if, while, and sequencing; and the OBox provides an oracle-sensitive layer for controlled external import. The judgments used in connection with these procedural and oracle-sensitive constructs do not themselves belong to the underlying description-logic language. They are metalevel relations specifying how guards are evaluated, how procedures are executed, and how externally obtained information is admitted into the current state. In concrete applications to information behavior, such judgments may be realized by a system, by a user, or by an oracle-mediated interaction process. This separation of layers is one of the essential features of TAPO-DL as developed here. To make this separation mathematically explicit, the paper introduces a guard-judgment layer for procedural branching and iteration. Instead of leaving if and while at the level of informal pseudocode, we give them proof-theoretic transition rules mediated by guard evaluation. This does not amount to a full internalization of procedural behavior into the object language of description logic; rather, it records at the metalevel how the procedural layer interacts with the static DL layer. In this respect the framework is intentionally hybrid: descriptive formulas remain in the DL layer, while procedural control is governed by judgments that are computationally meaningful and theoretically analyzable. The paper is organized as follows. In Section˜2 we recall the refined TAPO-DL architecture and fix the localized notation used throughout. In Section˜3 we sharpen the OBox by introducing admissible queries and responses, trust levels, certification data, and validation policies. In Section˜4 we present a core inference system for the refined framework, including the guard-judgment layer for the PBox. The categorical semantics is then developed in Sections˜5, 6, 7 and 8. We record a schematic soundness statement together with the associated completeness problem in Section˜9, and only after that turn to information-behavior examples in Section˜10, ranging from simple search behavior to review-sensitive ordering behavior in a curry restaurant. Finally, Section˜11 records further directions. 2. Refined TAPO-description logic 2.1. Signature, concepts, and contexts Let the TAPO-signature be Σsig=(NC,NR,NI,), _sig=(N_C,N_R,N_I,U), where NCN_C is a set of concept names, NRN_R a set of role names, NIN_I a set of individual names, and U is a collection of contextual domains. We regard U as a poset under refinement, writing V≤UV≤ U when V is a refinement of U. Concept expressions are generated by the usual ℒALC grammar C::=⊤∣⊥∣A∣C⊓D∣C⊔D∣¬C∣∃r.C∣∀r.C,C::= A C D C D C ∃ r.C ∀ r.C, with A∈NCA∈ N_C and r∈NRr∈ N_R. 2.2. The TAPO architecture A TAPO-knowledge state over a context U∈U consists of four layers: (U)=(,U,U,U). KB(U)=( T, A_U, P_U, O_U). Here: • T records terminological data, such as concept inclusions and structural axioms; • U A_U records contextual assertions valid over U; • U P_U records admissible procedures over the localized state (,U)( T, A_U); • U O_U records admissible modes of interaction with external information sources over U. The original logical motivation for this four-layer structure is given in [6]. 2.3. Localization and restriction Restriction along V≤UV≤ U is written ρUV:(U)→(V). _UV: KB(U)→ KB(V). At the skeletal level we require functoriality of restriction and compatibility with the four-layer TAPO decomposition. Definition 2.1 (Presheaf of TAPO-states). A presheaf of TAPO-states on U is a contravariant functor :op→ KB:U^op whose value (U) KB(U) is the set of TAPO-knowledge states over U. Remark 2.2. The point of using a presheaf already at this stage is that TBox/ABox/P/O-data need not be globally settled. Context dependence, partiality of information, and later gluing are built in from the start. 3. The OBox as oracle interface and controlled external import In the present reorganization, the oracle layer is refined before the proof theory and before the categorical semantics are unfolded in detail. This reflects the view that the strengthened OBox is one of the main formal innovations of the paper. The oracle layer is the place where the present paper most decisively strengthens the earlier logical skeleton from [6]. In the original paper, the OBox was presented at a minimal level by an externally justified transition relation ⟦⟧⊆(×)×(×). O ( T× A)×( T× A). Here we retain that intuition but replace it with a more structured semantics. 3.1. The strengthened OBox Definition 3.1 (Strengthened oracle frame). Let XU=(ΣU,U,U)X_U=( _U, P_U, O_U) with ΣU=(,U) _U=( T, A_U). A strengthened oracle frame over U consists of the following data: (1) a set QUQ_U of admissible queries; (2) a set RUR_U of admissible responses; (3) a partial answer map ansU:QU⇢RU;ans_U:Q_U R_U; (4) an import map impU:RU⇢(Asrt(U));imp_U:R_U (Asrt(U)); (5) a preordered set (LU,⪯)(L_U, ) of trust levels; (6) a trust assignment trU:RU→LU;tr_U:R_U→ L_U; (7) a certificate space CUC_U and certificate assignment certU:RU→(CU);cert_U:R_U (C_U); (8) a chosen trust threshold ℓU∈LU _U∈ L_U; (9) a validation policy valU(r,S)∈,,,val_U(r,S)∈\ accept, reject, defer\, defined for r∈RUr∈ R_U and finite certificate sets S⊆CUS C_U. Remark 3.2. Compared with the earlier TAPO-DL paper [6], the present formulation extends the OBox in four explicit directions: admissible queries and responses are separated; raw oracle answers are distinguished from imported assertions; trust and certification data are recorded; and a validation policy mediates which externally obtained information is actually integrated into the ABox. 3.2. Validated import Definition 3.3 (Validated response). A response r∈RUr∈ R_U is validated if there exists a finite set S⊆certU(r)S _U(r) such that trU(r)⪰ℓUandvalU(r,S)=.tr_U(r) _U _U(r,S)= accept. Definition 3.4 (Validated import map). The validated import map vimpU:RU⇢(U)vimp_U:R_U ( A_U) is defined exactly on validated responses and agrees there with the ordinary import map impUimp_U. Definition 3.5 (Sound strengthened OBox). A strengthened oracle frame is sound if every validated response imports only assertions compatible with the TBox T. Proposition 3.6 (Certified oracle transition). A sound strengthened oracle frame determines a partial endomap ωUval:ΣU⇢ΣU _U^val: _U _U by adjoining the validated imported assertions to U A_U whenever defined. Proof. If a response is validated, then by definition it passes the trust and certification threshold; if the frame is sound, its imported assertions are compatible with T. Hence the updated pair (,U′)( T, A_U ) is again a localized knowledge state. ∎ Remark 3.7. In this way the original transition-relation view of the OBox is recovered as a shadow of a more structured oracle mechanism. The present categorical skeleton therefore keeps the spirit of [6] while making the oracle layer mathematically more explicit. 3.3. Restriction compatibility Definition 3.8 (Restriction-compatible strengthened OBox). Let V≤UV≤ U. A strengthened oracle frame over U is restriction-compatible if there are induced maps QU→QV,RU→RV,LU→LV,CU→CV,Q_U→ Q_V, R_U→ R_V, L_U→ L_V, C_U→ C_V, such that answer maps, trust assignments, certificate assignments, validation policies, and validated import commute with restriction of localized knowledge states. Proposition 3.9 (Restriction of validated oracle imports). Suppose the strengthened OBox is restriction-compatible. Then validated oracle imports commute with contextual restriction wherever both sides are defined. Proof. This is exactly the content of restriction-compatibility: a response, its trust data, its certification data, and its validation status are all transported coherently along restriction, and validated import is required to commute with the restriction maps of the surrounding TAPO-presheaf. ∎ 3.4. Compositionality of oracle interfaces Definition 3.10 (Composable strengthened oracle frames). Two strengthened oracle frames on ΣU _U are composable if the validated output state of the first lies in the domain of the second whenever both are defined. Proposition 3.11 (Closure under certified composition). Let ω1 _1 and ω2 _2 be composable strengthened oracle frames. If the validation policy for ω2 _2 is allowed to inspect certificates produced or preserved by ω1 _1, then the composite oracle transition again admits a natural certified semantics. Proof. One composes the underlying partial transitions and carries the certification data produced at the first stage to the second-stage validation policy. Soundness is inherited provided each stage accepts only T-compatible imports. ∎ Remark 3.12. This again goes beyond the original OBox formulation in [6]. There the main point was controlled openness to external information. Here that openness is refined into a compositional interface with provenance-sensitive validation. Remark 3.13 (How the present OBox extends the original TAPO-DL layer). In the original TAPO-DL paper [6], the OBox was introduced mainly as a relation of externally justified state transition. The present paper keeps that basic idea, but extends it in a form better suited to information-behavior analysis. The extension has four visible aspects: the query posed by the agent is separated from the response returned by the external source; imported assertions are distinguished from raw responses; trust and certification are represented explicitly; and a validation policy determines which externally obtained content is actually integrated into the ABox. In this sense the strengthened OBox is not a different oracle layer, but a structured refinement of the original one. 3.5. Why the OBox is mathematically nontrivial The strengthened OBox is not merely a box labelled “outside information.” It carries at least five visible pieces of structure: admissible questions, admissible answers, an import mechanism, trust/certification data, and validation policies compatible with context. From a categorical viewpoint, the oracle layer behaves like a structured interface between an internal knowledge state and a family of external information channels. 4. A core inference system for TAPO-description logic The semantic skeleton developed above becomes substantially stronger once one records a corresponding proof-theoretic layer. We therefore introduce a small inference system whose purpose is to make explicit how static entailment, guard evaluation, procedural transition, and oracle-mediated import may be derived inside TAPO-description logic itself. A fuller completeness theorem is left for later refinement; the present calculus is intended as the core proof-theoretic layer compatible with the semantics developed here. 4.1. Judgments We use five kinds of judgments. (1) Terminological consequence: ⊢C⊑D. T C D. (2) Assertional consequence over a context U: ΣU⊢a:C@U,ΣU⊢(a,b):r@U. _U a:C@U, _U (a,b):r@U. (3) Static guard evaluation: (ΣU,U)⇓gγ:,(ΣU,U)⇓gγ:.( _U, P_U) _gγ:t, ( _U, P_U) _gγ:f. (4) Procedural transition: (ΣU,U)⊢P:ΣU↝ΣU′.( _U, P_U) P: _U _U . (5) Oracle-mediated validated import: (ΣU,U)⊢q⇒ΣU′.( _U, O_U) q V _U . The first two are static descriptive judgments. The third is a static guard judgment attached to the procedural layer and records whether a branching condition is currently evaluated as true or false. The fourth is dynamic and records state transformation by a PBox program. The fifth records validated acquisition of external information under a fixed validation policy V. 4.2. Static rules for the TBox and ABox The static core extends standard description-logic reasoning by context labels. Definition 4.1 (Static rules). The core static rules include the following schemata: ⊢C⊑DΣU⊢a:C@UΣU⊢a:D@U(T-Sub) T C D _U a:C@U _U a:D@U\;(T -Sub) ΣU⊢a:C@UΣU⊢a:D@UΣU⊢a:(C⊓D)@U(⊓I) _U a:C@U _U a:D@U _U a:(C D)@U\;( ) ΣU⊢a:(C⊓D)@UΣU⊢a:C@U(⊓E1)ΣU⊢a:(C⊓D)@UΣU⊢a:D@U(⊓E2) _U a:(C D)@U _U a:C@U\;( _1) _U a:(C D)@U _U a:D@U\;( _2) ΣU⊢(a,b):r@UΣU⊢b:C@UΣU⊢a:∃r.C@U(∃I) _U (a,b):r@U _U b:C@U _U a:∃ r.C@U\;( ) a:C@U∈UΣU⊢a:C@U(A-Ax)(a,b):r@U∈UΣU⊢(a,b):r@U(R-Ax) a:C@U∈ A_U _U a:C@U\;(A -Ax) (a,b):r@U∈ A_U _U (a,b):r@U\;(R -Ax) Remark 4.2. These rules are intentionally modest. Their role is to exhibit a static deductive layer compatible with the categorical semantics of Section˜6, not to provide a maximal calculus for all description-logic constructors. 4.3. Guard judgments as a distinct layer The distinction between static description and procedural control is essential in TAPO-DL. In particular, the branching constructs of the PBox are not ordinary formulas of description logic. They are governed by a separate guard judgment at the metalevel. Formally, this judgment belongs neither to the TBox/ABox object language nor to the oracle language. In concrete interpretations it may be realized by a system, by a user, or by an oracle-mediated interaction process. Definition 4.3 (Guard language and guard profile). Fix a context U. Let GUG_U be a designated set of basic guard atoms. In the present paper these may be chosen from localized assertions such as a:C@Ua:C@U or (a,b):r@U(a,b):r@U whenever they are intended to serve as branching conditions. The guard language UG_U is generated by γ::=α∣⊤∣⊥∣(γ∧γ)∣(γ∨γ)∣¬γ,α∈GU.γ::=α (γ γ) (γ γ) γ, α∈ G_U. A guard profile at U is a total assignment χU:GU→,. _U:G_U→\t,f\. The corresponding guard judgment (ΣU,U)⇓gγ:b(b∈,)( _U, P_U) _gγ:b (b∈\t,f\) is the least relation determined by χU _U together with the usual Boolean clauses: (ΣU,U)⇓gα:b⇔χU(α)=b,( _U, P_U) _gα:b _U(α)=b, (ΣU,U)⇓g⊤:,(ΣU,U)⇓g⊥:,( _U, P_U) _g :t, ( _U, P_U) _g :f, (ΣU,U)⇓g(γ1∧γ2):⇔(ΣU,U)⇓gγ1: and (ΣU,U)⇓gγ2:,( _U, P_U) _g( _1 _2):t ( _U, P_U) _g _1:t and ( _U, P_U) _g _2:t, (ΣU,U)⇓g(γ1∧γ2):⇔(ΣU,U)⇓gγ1: or (ΣU,U)⇓gγ2:,( _U, P_U) _g( _1 _2):f ( _U, P_U) _g _1:f or ( _U, P_U) _g _2:f, (ΣU,U)⇓g(γ1∨γ2):⇔(ΣU,U)⇓gγ1: or (ΣU,U)⇓gγ2:,( _U, P_U) _g( _1 _2):t ( _U, P_U) _g _1:t or ( _U, P_U) _g _2:t, (ΣU,U)⇓g(γ1∨γ2):⇔(ΣU,U)⇓gγ1: and (ΣU,U)⇓gγ2:,( _U, P_U) _g( _1 _2):f ( _U, P_U) _g _1:f and ( _U, P_U) _g _2:f, (ΣU,U)⇓g¬γ:⇔(ΣU,U)⇓gγ:,(ΣU,U)⇓g¬γ:⇔(ΣU,U)⇓gγ:.( _U, P_U) _g γ:t ( _U, P_U) _gγ:f, ( _U, P_U) _g γ:f ( _U, P_U) _gγ:t. Remark 4.4. The use of guard profiles avoids raw non-derivability conditions such as ⊬ inside the procedural rules. This is important both proof-theoretically and conceptually. Proof-theoretically, it keeps branching on the side of positive judgments. Conceptually, it makes explicit that the decision to take a branch belongs to a procedural control layer and need not be identified with ordinary description-logic entailment. 4.4. Transition rules for the PBox The procedural layer is naturally formulated by transition judgments rather than ordinary formula entailment. Its branching rules are defined relative to the guard judgment introduced above. Definition 4.5 (Core PBox transition rules). For programs in the language 0P_0, the following transition rules are admitted: (ΣU,U)⊢:ΣU↝ΣU(Skip) ( _U, P_U) : _U _U\;(Skip) (ΣU,U)⊢β:ΣU↝(,U∪β)(Add) ( _U, P_U) \;β: _U ( T, A_U∪\β\)\;(Add) (ΣU,U)⊢β:ΣU↝(,U∖β)(Del) ( _U, P_U) \;β: _U ( T, A_U \β\)\;(Del) (ΣU,U)⊢P:ΣU↝ΣU′(ΣU′,U)⊢Q:ΣU′↝ΣU′(ΣU,U)⊢P;Q:ΣU↝ΣU′(Seq) ( _U, P_U) P: _U _U ( _U , P_U) Q: _U _U ( _U, P_U) P;Q: _U _U \;(Seq) (ΣU,U)⇓gγ:(ΣU,U)⊢P:ΣU↝ΣU′(ΣU,U)⊢γPQ:ΣU↝ΣU′(If-T) ( _U, P_U) _gγ:t ( _U, P_U) P: _U _U ( _U, P_U) \;γ\;then\;P\;else\;Q: _U _U \;(If -T) (ΣU,U)⇓gγ:(ΣU,U)⊢Q:ΣU↝ΣU′(ΣU,U)⊢γPQ:ΣU↝ΣU′(If-F) ( _U, P_U) _gγ:f ( _U, P_U) Q: _U _U ( _U, P_U) \;γ\;then\;P\;else\;Q: _U _U \;(If -F) (ΣU,U)⇓gγ:(ΣU,U)⊢γP:ΣU↝ΣU(While-F) ( _U, P_U) _gγ:f( _U, P_U) \;γ\;do\;P: _U _U\;(While -F) (ΣU,U)⇓gγ:(ΣU,U)⊢P:ΣU↝ΣU′(ΣU′,U)⊢γP:ΣU′↝ΣU′(ΣU,U)⊢γP:ΣU↝ΣU′(While-T) array[]c( _U, P_U) _gγ:t\\ ( _U, P_U) P: _U _U \\ ( _U , P_U) \;γ\;do\;P: _U _U array( _U, P_U) \;γ\;do\;P: _U _U \;(While -T) Remark 4.6. The PBox rules express information behavior as derivable state change. In particular, a hesitation condition can lead not directly to a final assertion, but to a procedural branch, to repeated reformulation, or to invocation of the oracle layer. The guard judgment keeps explicit that such branching belongs to a distinct procedural control layer rather than to the descriptive core alone. 4.5. Validated import rules for the OBox The strengthened OBox from Section˜3 permits a proof-theoretic reading of trust-sensitive external import. Definition 4.7 (Core OBox rules). Let V be a validation policy. The core oracle rules are: q∈QUansU(q)=r(ΣU,U)⊢q↝r(Query) q∈ Q_U _U(q)=r( _U, O_U) q r\;(Query) (ΣU,U)⊢q↝rtrU(r)⪰ℓUvalU(r,S)=(ΣU,U)⊢q⇒(,U∪vimpU(r))(Oracle-Accept) ( _U, O_U) q r _U(r) _U _U(r,S)= accept( _U, O_U) q V( T, A_U _U(r))\;(Oracle -Accept) (ΣU,U)⊢q↝r(trU(r)⋡ℓU or valU(r,S)∈,)(ΣU,U)⊢q⇒ΣU(Oracle-Hold) ( _U, O_U) q r (tr_U(r) _U or val_U(r,S)∈\ reject, defer\ )( _U, O_U) q V _U\;(Oracle -Hold) for finite certificate sets S⊆certU(r)S _U(r). Remark 4.8. The rule (Oracle-Hold)(Oracle -Hold) is important for information-behavior analysis. An external review, recommendation, or report may be consulted without yet being imported; this corresponds formally to a derivable transition that leaves the current state unchanged. 4.6. Procedural invocation of the oracle layer The TAPO setting becomes distinctive when PBox and OBox judgments are allowed to interact. Definition 4.9 (Consultation rule). Assume that a procedural state records unresolved hesitation by an assertion of the form ΣU⊢x:@U. _U x: ReviewConsultationNeeded@U. Then an oracle consultation may be triggered by the rule ΣU⊢x:@U(ΣU,U)⊢qx⇒ΣU′(ΣU,U,U)⊢(qx):ΣU↝ΣU′(Consult) _U x: ReviewConsultationNeeded@U ( _U, O_U) q_x V _U ( _U, P_U, O_U) (q_x): _U _U \;(Consult) provided qxq_x is an admissible query associated with the hesitation state of x. Remark 4.10. Rule (Consult)(Consult) formalizes exactly the sort of situation illustrated by the curry-restaurant example in Example 10.6: uncertainty does not directly resolve into acceptance or rejection, but first triggers an external review query, whose validated result then re-enters the procedural flow. 5. TAPO-structured knowledge objects We now turn to the categorical semantics of the refined framework. The first step is to isolate the localized TAPO-objects on which the semantic constructions operate. In order to keep the categorical language close to the original TAPO-DL notation, we separate the static knowledge state ΣU=(,U) _U=( T, A_U) from the procedural and oracle layers attached to it. Definition 5.1 (Localized knowledge state). For a fixed context U∈U , a localized knowledge state is a pair ΣU=(,U), _U=( T, A_U), where T is a TBox and U A_U is a contextual ABox over U. Definition 5.2 (TAPO-object). A TAPO-object over U is a triple XU=(ΣU,U,U)X_U=( _U, P_U, O_U) consisting of a localized knowledge state ΣU=(,U) _U=( T, A_U), a procedural layer U P_U over ΣU _U, and an oracle layer U O_U over ΣU _U. Definition 5.3 (Morphisms of TAPO-objects). A morphism f:XU→YUf:X_U→ Y_U of TAPO-objects over the same context is a quadruple f=(fT,fA,fP,fO)f=(f_T,f_A,f_P,f_O) with the following properties: (1) fTf_T preserves valid terminological inclusions in the TBox; (2) fAf_A carries contextual assertions a:C@Ua:C@U and (a,b):r@U(a,b):r@U in U A_U to corresponding assertions in the target ABox; (3) fPf_P transports admissible PBox programs and preserves their evaluations whenever defined; (4) fOf_O transports admissible oracle interfaces and preserves validated oracle imports whenever defined. Definition 5.4 (Execution-stable morphism). A morphism f:XU→YUf:X_U→ Y_U is execution-stable if the following hold. (1) For every program P∈UP∈ P_U, the denotation of its transport fP(P)∈U′f_P(P)∈ P _U satisfies fA∘⟦P⟧U≃⟦fP(P)⟧U∘fAf_A P _U f_P(P) _U f_A wherever both sides are defined. (2) For every oracle interface ω∈Uω∈ O_U, the validated import transition of its transport fO(ω)f_O(ω) satisfies the analogous commutation relation with fAf_A. Proposition 5.5 (Category of TAPO-objects). For each fixed context U, TAPO-objects over U and execution-stable morphisms between them form a category. Proof. Identity morphisms are execution-stable by definition. If f:XU→YUf:X_U→ Y_U and g:YU→ZUg:Y_U→ Z_U are execution-stable, then preservation of TBox data, ABox assertions, program evaluations, and validated oracle imports is inherited by composition. Hence g∘fg f is again execution-stable. ∎ Remark 5.6. This formulation is closer to the original TAPO-DL presentation than the earlier quadruple-style description, because the PBox and OBox are now visibly attached to the localized state ΣU=(,U) _U=( T, A_U) on which they operate. 6. The TBox and ABox as categorical data The TBox and ABox form the static core of the theory. This is the part most closely aligned with existing category semantics for ordinary description logic [7, 2, 8]. 6.1. The TBox A TBox is interpreted as a system of structural constraints. In a category-theoretic language, concept inclusions may be read as arrows, subobjects, or designated entailment morphisms, depending on the semantic level one chooses. Definition 6.1 (Categorical TBox semantics). A categorical TBox semantics assigns to each concept symbol C an object ⟦C⟧ C and to each valid inclusion C⊑DC D in T a distinguished morphism ⟦C⟧⟶⟦D⟧ C D in a background category ℰE with sufficient logical structure. 6.2. The ABox The ABox records individuals and role assertions. In a categorical semantics this may be encoded by generalized elements, sections, or points relative to context. Definition 6.2 (Contextual ABox semantics). For each context U∈U , an assertion a:C@Ua:C@U is interpreted by a generalized element 1U⟶⟦C⟧(U),1_U C (U), and a role assertion (a,b):r@U(a,b):r@U is interpreted by a generalized element of the contextual relation object corresponding to r over U. Proposition 6.3 (Restriction of assertions). Let V≤UV≤ U in U. If a:C@Ua:C@U or (a,b):r@U(a,b):r@U is represented over U, then restriction induces a corresponding representation over V. In particular, contextual assertions are functorial under refinement. Proof. This is immediate from the contravariance of the presheaf associated with the relevant concept or relation object. ∎ Proposition 6.4 (Preservation under TAPO-morphisms). Let f:XU→YUf:X_U→ Y_U be a morphism of TAPO-objects. If f respects the distinguished morphisms associated with terminological inclusions and the generalized elements representing contextual assertions, then every TBox entailment or ABox assertion valid in XUX_U is carried to a corresponding valid entailment or assertion in YUY_U. Proof. The preservation of TBox data follows from functoriality on the distinguished entailment morphisms, and the preservation of ABox data follows from the image of the corresponding generalized elements under f. ∎ 7. The PBox as a minimal imperative layer We now move closer to the notation of the original TAPO-DL paper [6]. The PBox is not a set of inference rules, but a programmable layer over the localized knowledge state ΣU=(,U). _U=( T, A_U). 7.1. Guards Definition 7.1 (Guards). Guards over ΣU=(,U) _U=( T, A_U) are generated by φ::=⊤∣⊥∣α∣¬φ∣(φ∧φ), ::= α ( ), where atomic guards are of the form α::=a:C@U∣(a,b):r@U∣(C⊑D).α::=a:C@U (a,b):r@U (C D). Their satisfaction relation is defined by (,U)⊧a:C@U ( T, A_U) a:C@U ⇔a:C@U∈U, a:C@U∈ A_U, (,U)⊧(a,b):r@U ( T, A_U) (a,b):r@U ⇔(a,b):r@U∈U, (a,b):r@U∈ A_U, (,U)⊧(C⊑D) ( T, A_U) (C D) ⇔⊢DLC⊑D, T _DLC D, with Boolean connectives interpreted classically. 7.2. Program syntax Definition 7.2 (The minimal imperative language 0P_0). The language 0P_0 of localized PBox programs is generated by P::=∣β∣β∣P;P∣γP∣γP,P::=skip \;β \;β P;P \;γ\;then\;P\;else\;P \;γ\;do\;P, where β ranges over ABox assertions a:C@Ua:C@U and (a,b):r@U(a,b):r@U, and γ ranges over the guard language UG_U of Section˜4.3. Remark 7.3. This is exactly the style of programmable procedural layer emphasized in [6]. The categorical step taken here is not to alter the syntax, but to interpret such programs as partial endomaps of localized knowledge states. 7.3. Operational semantics and denotations We write ⟨P,ΣU⟩⇓ΣU′ P, _U _U for the big-step evaluation relation, understood relative to the guard profile carried by the current procedural configuration at U. Thus the clauses for conditionals and while-loops consult the guard judgment of Section˜4.3, while the remaining clauses are the usual ones for skip, add, del, and sequencing. Definition 7.4 (Program denotation). For each program P∈0P _0, its denotation at context U is the partial map ⟦P⟧U:ΣU⇢ΣU P _U: _U _U given by ⟦P⟧U(ΣU)=ΣU′⟺⟨P,ΣU⟩⇓ΣU′. P _U( _U)= _U P, _U _U. Definition 7.5 (PBox semantics). A PBox over U is a chosen class U⊆0 P_U _0 of admissible programs whose denotations are closed under the semantic operations that are intended to be available at context U. Proposition 7.6 (Sequential compositionality). If P1,P2∈UP_1,P_2∈ P_U and both denotations are defined on a localized state ΣU _U, then ⟦P2;P1⟧U=⟦P2⟧U∘⟦P1⟧U P_2;P_1 _U= P_2 _U P_1 _U wherever the composite is defined. In particular, the PBox carries an intrinsic compositional structure. Proof. This is the standard big-step semantics for sequencing. ∎ Proposition 7.7 (Closure under conditionals). Assume U P_U is closed under the program-forming operation (P1,P2,γ)⟼γP1P2.(P_1,P_2,γ) \;γ\;then\;P_1\;else\;P_2. Then every such conditional built from members of U P_U again belongs to U P_U. Proof. This is immediate from the closure assumption. ∎ Remark 7.8. The preceding proposition is the direct categorical analogue of the original TAPO-DL idea that conditionals are internal program constructors, not meta-level instructions. Definition 7.9 (Iterative partiality). For a guard γ and a program P∈UP∈ P_U, the loop γPwhile\;γ\;do\;P induces a partial endomap ⟦φP⟧U:ΣU⇢ΣU \; \;do\;P _U: _U _U which is defined exactly on those states for which the iteration terminates. Remark 7.10. Thus the PBox naturally accommodates partiality. This matches the original proof-theoretic intuition of TAPO-DL, where while-constructs need not terminate [6]. Proposition 7.11 (Restriction compatibility of procedures). Suppose V≤UV≤ U and the procedural layer is stable under contextual restriction. Then for every P∈UP∈ P_U there exists a restricted program P|V∈VP|_V∈ P_V such that ρUV∘⟦P⟧U≃⟦P|V⟧V∘ρUV _UV P _U P|_V _V _UV wherever both sides are defined. Proof. This is the procedural analogue of functoriality for contextual assertions. Stability under restriction provides the restricted program, and the commutation statement is precisely the assumed contextual compatibility. ∎ Remark 7.12. It is worth noting, as a nearby line of motivation rather than a direct semantic precursor, that recent work in NLP-assisted formal modeling has attempted to extract from natural-language specifications intermediate structures built from predicates, functions, and pre-/post-condition patterns [5]. From the present viewpoint, such representations are relevant mainly as a syntactic front end for procedural information. The role of the PBox in TAPO-description logic is different: it is meant to internalize that procedural layer as mathematical structure inside the logic itself. 8. Sheaf-theoretic refinement The presheaf picture suggests a genuine sheaf-theoretic strengthening. Definition 8.1 (Sheaf of TAPO-states). A presheaf of TAPO-states is a sheaf if locally compatible families of TAPO-objects admit unique gluing. Theorem 8.2 (Schematic local-to-global principle). Assume the TAPO-state assignment forms a sheaf on U, and assume that both procedural denotations and strengthened oracle frames are restriction-compatible. Then compatible local TAPO-updates glue to a global TAPO-update. Proof. At this stage the statement is schematic. The intended proof combines the sheaf condition for underlying local states with compatibility of PBox and OBox data under restriction. Once these data are formulated as morphisms in an appropriate fibred or internal category, the gluing follows from the corresponding descent condition. ∎ Remark 8.3. This is the point where a later topos-theoretic development becomes natural. Local knowledge, local procedures, and local oracle responses can then be studied internally, while global coherence is governed by descent. Remark 8.4. In particular, a trust- and certification-sensitive OBox suggests that descent should later be formulated not only for bare assertions, but also for validated provenance data. This would make the local-to-global passage sensitive to how imported information was certified, not merely to what was imported. 9. Soundness and the completeness problem The proof theory is intended as a companion to the semantic structures already introduced. Theorem 9.1 (Schematic soundness). Each of the preceding rules is sound with respect to the semantic skeleton of Sections˜6, 7 and 3. More precisely: (1) if ⊢C⊑D T C D or ΣU⊢α _U α is derivable by the static rules, then the corresponding categorical interpretation is valid in the sense of Section˜6; (2) if (ΣU,U)⊢P:ΣU↝ΣU′( _U, P_U) P: _U _U is derivable, then ⟦P⟧U(ΣU)=ΣU′ P _U( _U)= _U whenever the denotation is defined; (3) if (ΣU,U)⊢q⇒ΣU′( _U, O_U) q V _U is derivable, then ΣU′ _U coincides with the state produced by the validated oracle transition associated with the strengthened OBox. The mixed consultation rule is also sound: if (ΣU,U,U)⊢(qx):ΣU↝ΣU′,( _U, P_U, O_U) (q_x): _U _U , then the target state is exactly the one obtained by the validated oracle update triggered from the hesitation state of x. Proof. We argue by induction on the last rule used in the derivation. (1) Static rules. The axiom rules (A-Ax)(A -Ax) and (R-Ax)(R -Ax) are immediate from the contextual ABox semantics of Section˜6: an asserted judgment belongs to U A_U, hence is represented by the corresponding generalized element over U. For (T-Sub)(T -Sub), suppose that ⊢C⊑D T C D and ΣU⊢a:C@U _U a:C@U are both derivable. By the induction hypothesis, the premise a:C@Ua:C@U is interpreted by a generalized element 1U⟶⟦C⟧(U),1_U C (U), and the inclusion C⊑DC D is interpreted by a distinguished morphism ⟦C⟧⟶⟦D⟧ C D in the categorical TBox semantics. Composing these arrows yields a generalized element 1U⟶⟦D⟧(U),1_U D (U), which is exactly the interpretation of a:D@Ua:D@U. For (⊓I)( ), if a:C@Ua:C@U and a:D@Ua:D@U are both derivable, then by induction they are represented by generalized elements into ⟦C⟧(U) C (U) and ⟦D⟧(U) D (U). In the intended semantics, conjunction is interpreted by the categorical meet or product-like conjunction object, so these two arrows induce an arrow into ⟦C⊓D⟧(U) C D (U). This yields the soundness of conjunction introduction. The elimination rules (⊓E1)( _1) and (⊓E2)( _2) are then sound by composing with the corresponding projections. For (∃I)( ), assume that (a,b):r@U(a,b):r@U and b:C@Ub:C@U are derivable. By induction, we have a generalized element of the contextual relation object corresponding to r together with a generalized element of ⟦C⟧(U) C (U) for b. These data determine a witness for the existential condition, hence a generalized element interpreting a:∃r.C@Ua:∃ r.C@U. (2) Procedural rules. By Section˜7, the denotation ⟦P⟧U P _U is defined by the big-step evaluation relation ⟨P,ΣU⟩⇓ΣU′. P, _U _U . Thus each procedural rule is sound provided it agrees with the corresponding evaluation clause. The rule (Skip)(Skip) is sound because the operational semantics of skip leaves the state unchanged, so ⟦⟧U _U is the identity on localized knowledge states. The rules (Add)(Add) and (Del)(Del) are sound because they coincide exactly with adjoining or removing the indicated ABox assertion from the current state. For (Seq)(Seq), assume the premises derive (ΣU,U)⊢P:ΣU↝ΣU′and(ΣU′,U)⊢Q:ΣU′↝ΣU′.( _U, P_U) P: _U _U ( _U , P_U) Q: _U _U . By the induction hypothesis, ⟦P⟧U(ΣU)=ΣU′and⟦Q⟧U(ΣU′)=ΣU′. P _U( _U)= _U Q _U( _U )= _U . Hence the composite program satisfies ⟦P;Q⟧U(ΣU)=ΣU′, P;Q _U( _U)= _U , which is exactly the semantic content of the sequencing rule. This is the same compositionality recorded in Section˜7. For (If-T)(If -T), if (ΣU,U)⇓gγ:( _U, P_U) _gγ:t is derivable, then the guard judgment selects the then-branch. By induction on the premise for P, the resulting state is ⟦P⟧U(ΣU) P _U( _U), so the entire conditional has that same denotation. The case (If-F)(If -F) is analogous, except that the guard judgment derives f and the else-branch is selected. For (While-F)(While -F), if (ΣU,U)⇓gγ:( _U, P_U) _gγ:f, then the loop terminates immediately and the target state remains ΣU _U, exactly as stated by the rule. For (While-T)(While -T), assume that (ΣU,U)⇓gγ:( _U, P_U) _gγ:t, that (ΣU,U)⊢P:ΣU↝ΣU′,( _U, P_U) P: _U _U , and that (ΣU′,U)⊢γP:ΣU′↝ΣU′.( _U , P_U) \;γ\;do\;P: _U _U . By the induction hypothesis, the first procedural premise is interpreted by ⟦P⟧U(ΣU)=ΣU′ P _U( _U)= _U , and the second by the denotation of the loop started from ΣU′ _U . Hence the entire loop is interpreted by first executing one step of P and then iterating again. This is exactly the operational reading of the loop under guard-driven big-step evaluation. (3) Oracle rules. For (Query)(Query), the conclusion merely records the value of the partial answer map ansUans_U. Hence any derivable query-response judgment agrees with the strengthened oracle frame by definition. For (Oracle-Accept)(Oracle -Accept), assume that (ΣU,U)⊢q↝r,trU(r)⪰ℓU,valU(r,S)=.( _U, O_U) q r, _U(r) _U, _U(r,S)= accept. Then r is a validated response in the sense of Section˜3. Therefore vimpU(r)vimp_U(r) is defined and agrees with impU(r)imp_U(r) on that response. The conclusion of the rule is precisely the state obtained by adjoining the validated imported assertions to U A_U. By the soundness requirement imposed on strengthened OBoxes, those imported assertions remain compatible with T, so the target is again a legitimate localized state. Hence the rule agrees exactly with the certified oracle transition of Section˜3. For (Oracle-Hold)(Oracle -Hold), either the trust threshold is not met or the validation policy rejects or defers the response. In all such cases the validated import map is undefined, so no new ABox information may be integrated. The semantic effect is therefore the identity transition on ΣU _U, exactly as stated by the rule. (4) The consultation rule. Assume that the last rule is (Consult)(Consult). Then we have a derivation of ΣU⊢x:@U _U x: ReviewConsultationNeeded@U and a derivation of (ΣU,U)⊢qx⇒ΣU′.( _U, O_U) q_x V _U . By the static soundness already proved, the hesitation assertion is semantically valid in the current state. By oracle soundness, the second premise identifies ΣU′ _U with the output of the validated oracle update associated with qxq_x. The consultation rule does not add any independent semantic transformation beyond triggering that validated update from an admissible hesitation state. Therefore the conclusion (ΣU,U,U)⊢(qx):ΣU↝ΣU′( _U, P_U, O_U) (q_x): _U _U is sound. This completes the induction. ∎ Remark 9.2. A full completeness theorem is deliberately postponed. The present place in the exposition is intentional: once both the inference layer and the categorical semantics have been displayed, the completeness problem can be stated in its proper form. In particular, any later completeness treatment should separate the static guard layer from the dynamic transition layer and explain how guard profiles are fixed or generated. Because the present paper is centered on categorical semantics and information behavior rather than on a maximal proof calculus, the main point here is to show that TAPO-description logic already supports a coherent core of derivable static, guard-based procedural, and oracle-sensitive judgments. 10. Information-behavior examples and discussion The preceding framework is intended for the analysis of information behavior rather than for static ontology management alone. We therefore gather in one place a sequence of examples that illustrate how the refined TAPO-DL architecture treats procedural hesitation, external consultation, validation-sensitive import, and final action. 10.1. Simple search behavior The first group of examples models elementary information-seeking behavior. The point is that even a simple search episode already involves more than a static TBox/ABox-description: the agent may need procedural reformulation, iterative stabilization, and validated import of externally retrieved material. In this respect the examples are also close in spirit to Chang’s account of browsing as a multidimensional activity rather than a purely query-driven terminal act [4, 10]. Example 10.1 (Information-seeking episode as a PBox program). Let U be a context representing the current information need of an agent. Assume that the localized ABox contains assertions of the form q:@U,q:@U,s:@U.q: Query@U, q: Underspecified@U, s: SearchSession@U. Consider the guard atom γref:=q:@U _ref:=q: Underspecified@U viewed as an element of the designated basic guard set GUG_U, and the program Pseek:=γrefq:@Uq:@U.P_seek:=if\; _ref\;then\;add\;q: NeedsRefinement@Uelse\;add\;q: ReadyForRetrieval@U. Its denotation distinguishes two information-behavioral situations. If the guard judgment derives (ΣU,U)⇓gγref:,( _U, P_U) _g _ref:t, then the state is updated so as to record the need for reformulation; if it derives f, then the state is updated so as to permit retrieval. In this way, the PBox does not merely describe a search action externally, but internalizes the agent’s procedural decision rule inside the localized TAPO-state. Example 10.2 (Iterative stabilization of a search process). Still over a context U, suppose that the ABox may contain assertions q:@U,q:@U,q:@U.q: NeedsRefinement@U, q: ReadyForRetrieval@U, q: StableResultSet@U. Let Previse:=q:@U;q:@UP_revise:=del\;q: NeedsRefinement@U;add\;q: ReadyForRetrieval@U and consider the loop ¬(q:@U)Previse.while\; (q: StableResultSet@U)\;do\;P_revise. Here the negated guard is evaluated by the guard judgment of Section˜4.3. As long as (ΣU,U)⇓g¬(q:@U):,( _U, P_U) _g (q: StableResultSet@U):t, the revision step is executed and the loop continues; once the same judgment yields f, the loop terminates via (While-F)(While -F). This gives a simple model of iterative information behavior: the agent repeatedly revises the search state until a stable result set is reached. The loop may remain partial, reflecting the familiar fact that information seeking need not converge in finitely many steps. Example 10.3 (Validated external retrieval in information behavior). Let U encode an active literature-search context. Suppose that the current localized state contains q:@U,t:@U,r:@U.q: ReadyForRetrieval@U, t: Topic@U, r: ResultCandidate@U. An admissible query in QUQ_U asks an external bibliographic service for references relevant to t. A response ρ∈RUρ∈ R_U may contain candidate assertions such as r:(t)@U,r:@U,r:@U.r: RelevantTo(t)@U, r: PeerReviewed@U, r: RecentSource@U. The strengthened OBox treats these assertions as importable only after validation. For example, the validation policy may require both a sufficient trust level and a certificate that the source metadata is complete. Only then are the imported assertions adjoined to the ABox. Thus the OBox models a basic informational distinction between retrieved material and accepted material. Example 10.4 (Trust-sensitive oracle use for credibility assessment). Let U represent a fact-checking context in which an agent is evaluating a claim c. Assume that responses may carry trust labels such as ≺ low medium high and certificates recording provenance, timestamp, or source agreement. A validation policy can then require, for instance, that a response supporting c be accepted only if its trust level is at least medium and at least one provenance certificate is present. In that case, the OBox does not merely import information from outside; it records a mathematically explicit policy by which the agent discriminates between usable and non-usable external information. This is precisely the kind of informational evaluation that motivated the passage from TBox/ABox-structured to TAPO-structured description logic. 10.2. Review-sensitive ordering behavior in a curry restaurant The next examples show the same architecture in a more everyday setting. Menu labels produce impressions, those impressions trigger procedural branching, and online reviews function as oracle-type external input whose import is governed by trust and validation. The interaction between the procedural and oracle layers becomes clearer when one considers an everyday information-behavioral situation in which menu perception, hesitation, review consultation, and final action are intertwined. See Figure˜1 for a schematic overview of this passage from menu data to final ordering behavior. Menu / T-A data spice labels descriptions visible dishes Formed impressions safe balanced risky but authentic PBox avoid compare hesitate modify OBox consult reviews validate trust import accepted cues Final action order mild curry or balanced curry or vindaloo with reduced spice if undecided Figure 1. Information-behavior flow in the curry restaurant example. Menu data first generate localized impressions; these are then processed procedurally in the PBox, possibly supplemented by validated review input through the OBox, before a final ordering action is reached. Example 10.5 (Curry menu perception, review consultation, and ordering behavior). Let U be a dining context in which two customers u and v face the same curry menu. Suppose the localized ABox contains assertions of the form u:@U,v:@U,u: Customer@U, v: Customer@U, c1:@U,c2:@U,c3:@U,c_1: Curry@U, c_2: Curry@U, c_3: Curry@U, together with c1:@U,c2:@U,c3:@U.c_1: LowSpice@U, c_2: MediumSpice@U, c_3: HighSpice@U. Assume moreover that the menu descriptions induce the assertions c1:@U,c2:@U, c_1: GentleMenuImpression@U, c_2: BalancedMenuImpression@U, c3:@U. c_3: AuthenticMenuImpression@U. and that the high-spice marking of c3c_3 also yields c3:@U.c_3: RiskyMenuImpression@U. Thus the same dish c3c_3 is perceived under two competing aspects: it appears attractive as authentic, but risky as very hot. This tension is precisely the kind of localized informational state that cannot be expressed by the TBox/ABox core alone. Example 10.6 (PBox and OBox interaction in review-sensitive ordering). Continue Example˜10.5. Let the procedural layer contain a basic guard atom γrisk:=c3:@U _risk:=c_3: RiskyMenuImpression@U and a composite guard γundec:=u:@U∨v:@U. _undec:=u: UndecidedCustomer@U v: UndecidedCustomer@U. For the customer u, who does not consult external reviews, consider the program Pu:= P_u= γriskc3:@U \; _risk\;then\;add\;c_3: AvoidCandidate@U c3:@U;c1:@U. \;add\;c_3: PreferredCandidate@U;\ add\;c_1: SafeCandidate@U. Its denotation models a cautious ordering strategy: if the guard judgment derives (ΣU,U)⇓gγrisk:( _U, P_U) _g _risk:t, then the strong-spice dish c3c_3 is excluded from the candidate set; otherwise the mild dish c1c_1 is promoted as the safe fallback. For the customer v, by contrast, the procedural layer contains an intermediate step Pv:= P_v= (γrisk∧γundec)v:@U \;( _risk _undec)\;then\;add\;v: ReviewConsultationNeeded@U c2:@U. \;add\;c_2: BalancedCandidate@U. This means that the risk-impression attached to c3c_3 does not yet force rejection. Instead, when the guard judgment derives (ΣU,U)⇓g(γrisk∧γundec):( _U, P_U) _g( _risk _undec):t, it triggers an information-seeking action that activates the oracle layer. Now let q1∈QUq_1∈ Q_U ask whether the local meaning of “spice level 3” is milder than expected, and let q2∈QUq_2∈ Q_U ask whether the dish c3c_3 can be made less spicy on request. Suppose the oracle returns responses r1,r2∈RUr_1,r_2∈ R_U such that impU(r1)=c2:@U,imp_U(r_1)=\c_2: MilderThanExpected@U\, impU(r2)=c3:@U.imp_U(r_2)=\c_3: AdjustableOnRequest@U\. Assume further that r1r_1 and r2r_2 both satisfy the relevant trust threshold and validation policy, so that they are accepted by the strengthened OBox and imported into the localized ABox. After this validated oracle import, the procedural layer may continue with Pv′:= P_v = c3:@Uc3:@U \;c_3: AdjustableOnRequest@U\;then\;add\;c_3: ControllableCandidate@U c2:@U. \;add\;c_2: BalancedCandidate@U. Again the branching is governed by the guard judgment associated with the updated procedural configuration. Thus the ordering behavior of v differs essentially from that of u. Customer u, who relies only on menu perception, may end with the mild order u:(c1)@U,u: Orders(c_1)@U, whereas customer v, after trusted review consultation, may reach either v:(c2)@Uv: Orders(c_2)@U as a balanced choice, or even v:(c3)@U,v:(c3)@U.v: Orders(c_3)@U, v: ReducedSpiceRequest(c_3)@U. This example illustrates the informational reason for passing from TBox/ABox-structured to TAPO-structured description logic. The TBox/ABox layers record the menu and its explicit labels; the PBox records hesitation, candidate selection, and procedural branching; and the OBox records the import of external review information under a trust-sensitive validation policy. Online reviews therefore function here as a genuine oracle-like source: they do not merely add extra assertions, but alter how menu information is interpreted and how the final ordering action is procedurally determined. Remark 10.7. The curry example is intentionally elementary, but it already displays the information-behavioral content of TAPO-description logic. A single menu label can produce competing impressions; those impressions can trigger procedural hesitation rather than immediate action; and external review material can then enter the state only after validation. In this way, the final behavior is governed not by static data alone, but by the interaction of description, procedure, and oracle-sensitive evaluation. Remark 10.8. Taken together, the search examples and the curry examples show why the passage from TBox/ABox-structured to TAPO-structured description logic is not merely decorative. The TBox/ABox core records explicit descriptions; the PBox records hesitation, branching, revision, and candidate management; and the OBox records the admission of external material under explicit validation conditions. This is exactly the level at which one can begin to analyze and evaluate information behavior rather than merely describe information objects. 11. Further directions This paper is intentionally skeletal. Its aim is to prepare a mathematically usable categorical language for TAPO-description logic while keeping clear distance from a mere literature review. The next steps seem to include at least the following: (1) a precise base category or topos in which concepts, individuals, programs, and strengthened oracle frames all live internally; (2) a fuller proof theory, including completeness questions, normalization issues, and a more systematic comparison with the original TAPO-DL framework of [6]; (3) a richer internal treatment of trust, certification, provenance, and validation in the oracle layer; (4) richer families of examples showing how PBox and OBox data interact in concrete information-behavior scenarios, especially when procedural updates depend on validated external input and trust-sensitive review material. The present paper should therefore be read as a categorical first step beyond the original logical formulation [6], and as a bridge from ordinary categorical semantics of description logic to a broader TAPO-structured theory of information behavior. References [1] F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. F. Patel-Schneider (eds.), The Description Logic Handbook, 2nd ed., Cambridge University Press, Cambridge, 2010. [2] L. Brieulle, C. Le Duc, and P. Vaillant, Reasoning in the description logic ℒALC under category semantics, arXiv preprint arXiv:2205.04911, 2022. [3] S.-J. L. Chang, User friendly websites: information organization and browsing interface design issues: a case study of the Amazon.com, University Library Journal 5 (2001), 16–32. [4] S.-J. Chang and R. E. Rice, Browsing: a multidimensional framework, Annual Review of Information Science and Technology 28 (1993), 231–276. [5] S. Ghosh, A. Singh, A. Merenstein, W. Su, S. A. Smolka, E. Zadok, and N. Balasubramanian, SpecNFS: A challenge dataset towards extracting formal models from natural language specifications, in Proceedings of the 13th Conference on Language Resources and Evaluation (LREC 2022), Marseille, 2022, p. 2166–2176. [6] T. Inoué, TAPO-Structured Description Logic for Information Behavior: Procedural and Oracle-Based Extensions, Daigaku Kyoiku 9 (2026), 97–108, Yamato University. ISBN 978-4-9910161-8-9. Also, arXiv:2602.17242. [7] C. Le Duc, Category-theoretical semantics of the description logic ℒALC, arXiv preprint arXiv:2110.08837, 2021. [8] C. Le Duc and L. Brieulle, A new tractable description logic under categorical semantics, arXiv preprint arXiv:2505.08916, 2025. [9] S. Mac Lane and I. Moerdijk, Sheaves in Geometry and Logic, Springer, New York, 1992. [10] R. E. Rice, M. McCreadie, and S.-J. L. Chang, Accessing and Browsing Information and Communication, MIT Press, Cambridge, MA, 2001. [11] E. Patterson, Knowledge representation in bicategories of relations, arXiv preprint arXiv:1706.00526, 2017. Appendix A TAPO-Description Logic as a Formal Analytic Layer for Browsing Theory The purpose of this appendix is to indicate that the present framework is not only a formal system for information behavior in the abstract, but may also serve as an analytic layer for established theories of browsing. In particular, multidimensional approaches to browsing, such as those associated with Chang and collaborators [4, 10], suggest that browsing should not be reduced to a weak or incomplete form of direct searching. Rather, browsing is shaped by context, motivation, cognitive stance, available resources, and interface structure. From the present viewpoint, these aspects can be reorganized in a TAPO-structured manner and thereby made accessible to formal comparison and rule-based analysis. A.1. Why Chang-style browsing is relevant here A central lesson of the browsing literature is that information behavior often unfolds without a fully fixed query or a fully specified target state. Users may begin with only a vague interest, a tentative orientation, or a partially formed need, and the process may involve repeated inspection, comparison, hesitation, redirection, and opportunistic selection. Moreover, browsing behavior is influenced not only by the informational objects themselves, but also by the manner in which they are organized and displayed, the interface affordances available to the user, and the external evaluative cues encountered during the process [4, 3]. This perspective is highly compatible with the present development. If one works only with a TBox/ABox description-logic layer, one may represent concepts, instances, and static relational facts, but it becomes difficult to express the procedural unfolding of browsing or the selective use of external evaluative inputs. The introduction of the PBox and OBox is therefore not merely an optional extension: it is precisely what allows one to treat browsing as a dynamic and context-sensitive information behavior. A.2. A TAPO reinterpretation of multidimensional browsing Let U be a local informational context, for example a current interface state, a shelf region, a webpage category, or a visible result cluster. A TAPO-structured browsing state over U is written XU=(ΣU,U,U),ΣU=(,U).X_U=( _U, P_U, O_U), _U=( T, A_U). Figure 2 summarizes the basic TAPO reinterpretation of a Chang-style browsing episode. Local browsing context U interface state, shelf region, webpage category, visible result cluster TBox/ABox level static organizational structure and local instantiated facts visible items, categories, links, hesitation, candidate status OBox reviews, rankings, recommendations, trust assignment, certification, validation policy PBox inspect, compare, follow link, save candidate, return, refine interest procedural browsing behavior Browsing outcome stabilized candidate set, selected item, postponed decision, redirected exploration Figure 2. A TAPO reinterpretation of multidimensional browsing in the sense of Chang and collaborators. Static organizational structure is represented at the TBox/ABox level, browsing actions at the PBox level, and selectively incorporated external cues at the OBox level. We now reinterpret central ingredients of browsing theory within this structure. TBox layer. The TBox may contain concepts such as ,,,, Document,\ Category,\ VisibleItem,\ ProminentItem, ,,,, CandidateItem,\ RelevantItem,\ TrustedCue,\ ReviewSignal, InterfaceElement as well as roles such as (x,U),(x,C),(x,y), displayedIn(x,U),\ belongsTo(x,C),\ linkedTo(x,y), (x,y),(x,κ) recommendedWith(x,y),\ hasCue(x,κ) At this level, one captures the relatively stable classificatory and relational structure within which browsing takes place. ABox layer. The ABox records the current local informational facts, for example d1:@U,d2:@U,(d1,d2):@U,d_1: VisibleItem@U, d_2: ProminentItem@U, (d_1,d_2): linkedTo@U, or u:@U,(u,d1):@U,(u,d2):@U.u: User@U, (u,d_1): inspects@U, (u,d_2): hesitatesOver@U. Thus the ABox gives the presently instantiated browsing situation. PBox layer. The PBox represents the procedural side of browsing. This is crucial. Browsing is typically not a single inference step from query to answer, but a process involving actions such as: ,,,,,,,. inspect,\ compare,\ scroll,\ followLink,\ openPreview,\ saveCandidate,\ return,\ refineInterest. Accordingly, one may introduce guarded procedures such as (d)(d),if\ prominent(d)\ then\ inspect(d), (u)(d1,d2),if\ uncertain(u)\ then\ compare(d_1,d_2), (d)(d),if\ candidate(d)\ then\ save(d), _(u)_.while\ not\_settled(u)\ do\ browse\_next. Here the symbols (d) prominent(d), (u) uncertain(u), (d) candidate(d), and _(u) not\_settled(u) should be read as guard expressions evaluated by the metalevel guard judgment of Section˜4.3. This layer is what makes it possible to model browsing as an unfolding course of action rather than as a single declarative fact. OBox layer. The OBox represents the selective incorporation of external inputs. In a browsing setting, such external inputs include: reviews, recommendations, popularity signals, other users’ annotations, staff suggestions, or system-generated rankings. These are not merely additional assertions. They are externally sourced signals, often heterogeneous in reliability, and therefore naturally fall under the refined OBox: query, response, trust assignment, certification data, validation policy, and validated import. In this perspective, a browsing system may issue a query q=“Is item d widely regarded as useful for topic T?”q=``Is item $d$ widely regarded as useful for topic $T$?′ and receive one or more responses ρ. Only after trust-sensitive validation does the response become importable into the current knowledge state. Thus one may obtain an update of the form (ΣU,U)⊢q⇒ΣU′,( _U, O_U) q V _U , where the imported information is not raw testimony, but already filtered through a validation policy. A.3. Formal decomposition of browsing dimensions Chang-style browsing theory is valuable partly because it does not treat browsing as one-dimensional. The present framework suggests the following analytic decomposition. (1) Contextual dimension. This corresponds to the local site U and to the contextual assertions carried by U A_U. Examples include the current page, the shelf segment under inspection, or the visible cluster of results. (2) Behavioral dimension. This is captured by the PBox, whose rules describe movement, comparison, postponement, revisiting, and selection. (3) Motivational and cognitive dimension. This may be formalized by assertions such as u:@U,u:@U,u:@U,u: Undecided@U, u: Curious@U, u: RiskAverse@U, which then function as guards in the PBox. (4) Resource dimension. Available cues, recommendations, reviews, or interface affordances may be represented either as TBox/ABox-level objects or, when externally supplied and selectively incorporated, through the OBox. (5) Consequential dimension. The end result of a browsing episode need not be a single retrieved answer. It may instead be a transformed candidate set, a revised preference ordering, a narrowed region of attention, or a decision to postpone commitment. These are naturally represented as resulting TAPO-states after procedural and oracle-mediated updates. The point of this decomposition is not terminological. It shows that browsing theory can be made formally articulate: different dimensions correspond to different logical layers, and their interaction may be studied explicitly. A.4. A generic browsing episode in TAPO form We now sketch a generic browsing episode. Suppose the user begins in a state XU=(ΣU,U,U),X_U=( _U, P_U, O_U), where the ABox includes visible items d1:@U,d2:@U,d_1: VisibleItem@U, d_2: VisibleItem@U, and a hesitation assertion u:@U.u: Undecided@U. At the PBox level one may have a rule (u)(d1,d2).if\ Undecided(u)\ then\ compare(d_1,d_2). Suppose the corresponding guard judgment evaluates (u) Undecided(u) as true. If the comparison produces no stable preference, so that the guard judgment also evaluates _(u) still\_undecided(u) as true, then the following procedural rule is activated: _(u)(qd1,d2).if\ still\_undecided(u)\ then\ consult(q_d_1,d_2). This is precisely where the OBox becomes relevant. A query is issued, for example: qd1,d2=“Which of d1,d2 is more useful for topic T?”q_d_1,d_2=``Which of $d_1,d_2$ is more useful for topic $T$?′ The system or environment returns responses ρ1,ρ2,… _1, _2,… with associated trust values and possibly certification data. A validation policy V selects which responses may be imported. If the validated import yields d1:@U,d_1: RecommendedItem@U, then a further PBox rule may update the candidate structure: d1:@U(d1).if\ d_1: RecommendedItem@U\ then\ saveCandidate(d_1). Thus the browsing process is not modeled as an unstructured sequence of impressions, but as a controlled alternation between internal procedural moves and validated external enrichment. A.5. Why this goes beyond a descriptive restatement One may ask whether this appendix merely restates browsing theory in formal notation. The answer is no. The gain of the TAPO perspective is at least fourfold. First, it distinguishes clearly between static classificatory structure and procedural behavior. Many descriptions of browsing intermix these. In TAPO-description logic, the distinction between TBox/ABox and P is explicit. Second, it separates internal browsing behavior from externally supplied evaluative cues. This is the contribution of the refined OBox. Reviews, rankings, and recommendations do not simply become facts; they become validated imports. Third, it makes comparison possible. Different interface environments, different validation policies, or different user dispositions can be represented by different TAPO-configurations, and their consequences can then be compared. Fourth, it opens the way to proof-theoretic and semantic analysis. Once browsing is represented by judgments, procedural transitions, and oracle-sensitive imports, one may ask not only what happens, but under which rules it follows, whether certain outcomes are derivable, and how those derivations correspond to the categorical semantics. A.6. Relation to interface-sensitive browsing This formalization is especially suggestive for interface-sensitive studies of browsing. If item prominence, grouping, labeling, or recommendation widgets affect user behavior, then such influence may be represented at two levels. At the TBox/ABox level, the interface provides visible organizational structure. At the PBox level, this structure induces or biases procedures of inspection and navigation. At the OBox level, externally generated ratings, reviews, or recommendation signals enter the process selectively. Hence the present framework may be viewed as a mathematical apparatus for analyzing how organization, interface, and external cues jointly shape browsing behavior. A.7. Toward a formal research program The foregoing observations suggest that TAPO-description logic may support an independent research program on the formal analysis of browsing theory. At least the following questions appear natural: (1) Which classes of browsing episode can be represented by finite PBox procedures? (2) Under what conditions do repeated browsing and external consultation stabilize to a fixed candidate set? (3) How does one compare two interface environments in terms of the procedural and oracle-sensitive paths they induce? (4) Can one define formal notions of browsing success, serendipitous discovery, or premature abandonment within TAPO-structured knowledge dynamics? (5) To what extent can local browsing episodes be glued into a larger global account of information behavior via sheaf-theoretic methods? These questions go beyond the immediate scope of the present paper, but they indicate that the framework developed here is not merely compatible with browsing theory: it can also serve as a basis for a more formal and comparative theory of browsing itself. Remark A.1. From this perspective, the present paper may be read in two complementary ways. On the one hand, it develops TAPO-description logic as a logic for information behavior. On the other hand, it suggests that established theories of browsing, especially multidimensional and interface-sensitive ones, may be reinterpreted within TAPO-description logic as formally analyzable systems of local knowledge states, procedural transitions, and validated external inputs.