发表机构
DeepLethe（DeepLethe）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
PULSE是一种受对象-过程-方法论启发的可执行合约语言，经Lean 4等验证，在时空知识图谱工程中可实现证据约束等功能，能匹配工作流、区分变异体，在NOAA数据集上表现良好。
AI 中文摘要
知识图谱工程通常将已接受的状态、观测结果、约束、过程和假设场景分散在各个构件中，而这些构件的组合执行合约仍处于外部状态。我们提出PULSE，一种受对象-过程-方法论（Object-Process-Methodology）启发的语言，它在一个类型化运行时中定位了四种操作角色及其写入效果。此处的模式表示操作角色，而非模态或道义逻辑。该实现的合约固定了证据不可覆盖、分支隔离、基于事实的多主体计时器、受保护的状态变化以及时空上按声明排序的事件排序；外部运行器仍决定证据是否成为权威操作。GeoSPARQL、SOSA和SHACL仍为生成的视图。核心演算给出了效果约束引理和六个安全属性。Lean 4检查内核对应项的位置、证据、时钟、监视器、原子性和分支源保留；88个测试、3534个有界检查以及32个Lean/Python运行时内核案例将实现声明绑定到已检查的案例。第一作者实现了一个标准组合和一个独立的Sismic状态图，重现了经过测试的冷链轨迹。在37440个生成的时间轨迹中，PULSE匹配一个独立工作流并区分十个单字段变异体。在1980年以来的完整NOAA IBTrACS子集上，它与GEOS和事件扫描在1476290个过渡区对上达成一致，包括4800个采样事件和12831个时长符合要求的事件。特定项目的GeoSPARQL探针测量接口覆盖率。总体而言，结果支持所测试片段的合约定位、安全论证和轨迹对等性；语言的优越性和可用性未包含在评估范围内。
英文摘要
Knowledge graph engineering often distributes accepted state, observations, constraints, processes, and hypothetical scenarios across artifacts whose combined execution contract remains external. We present PULSE, an Object-Process-Methodology-inspired language that localizes four operational roles and their write effects in one typed runtime. Here, modes denote operational roles rather than modal or deontic logic. The implemented contract fixes evidence non-overwrite, branch isolation, grounded multi-subject timers, guarded state change, and declaration-ranked event ordering over time and space; an external runner still decides whether evidence becomes an authoritative move. GeoSPARQL, SOSA, and SHACL remain generated views. A core calculus gives an effect-confinement lemma and six safety properties. Lean 4 checks kernel analogues for positions, evidence, clocks, monitors, atomicity, and branch source retention; 88 tests, 3,534 bounded checks, and 32 Lean/Python runtime-kernel cases bound the implementation claim to the checked cases. First-author implementations of a standards composition and a separate Sismic statechart reproduce the tested cold-chain trace. Across 37,440 generated temporal traces, PULSE matches a separate workflow and distinguishes ten single-field mutants. On the complete NOAA IBTrACS since1980 subset it agrees with GEOS and an event sweep on 1,476,290 transition-zone pairs, including 4,800 sampled and 12,831 duration-qualified events. Project-specific GeoSPARQL probes measure interface coverage. Overall, the results support contract localization, safety arguments, and trace parity for the tested fragment; language superiority and usability remain outside the evaluation.
Comments6 pages, 5 tables, 1 code listing; submitted to KGSWC 2026. Research artifact available under the Apache-2.0 license
