This paper presents a formal framework for sequencing instructions in AI agents, inspired by the Indian philosophical system of Mimamsa. The framework formalizes sequencing mechanisms through action object pairs in three distinct ways: direct assertion (Srutikrama) for temporal precedence, purpose driven sequencing (Arthakrama) for functional dependencies, and iterative procedures (Pravrittikrama) for distinguishing between parallel and sequential execution in repetitive tasks. It introduces the syntax and semantics of an action object imperative logic, extending the MIRA formalism (Srinivasan and Parthasarathi, 2021) with explicit deduction rules for sequencing. The correctness of instruction sequencing is established through a validated theorem, which is based on object dependencies across successive instructions. This is further supported by proofs of soundness and completeness. This formal verification enables reliable instruction sequencing, impacting AI applications across areas like task planning and robotics by addressing temporal reasoning and dependency modeling.
翻译:本文提出了一种受印度弥曼差哲学体系启发的AI智能体指令排序形式化框架。该框架通过动作-对象对以三种不同方式形式化排序机制:用于时序优先关系的直接断言法(Srutikrama)、用于功能依赖性的目的驱动排序法(Arthakrama),以及用于区分重复任务中并行与顺序执行的迭代过程法(Pravrittikrama)。本文引入了动作对象命令逻辑的语法与语义,通过显式排序演绎规则扩展了MIRA形式化体系(Srinivasan与Parthasarathi, 2021)。指令排序的正确性通过基于连续指令间对象依赖关系的验证定理得以确立,并辅以可靠性与完备性证明。这种形式化验证实现了可靠的指令排序,通过处理时序推理与依赖建模,对任务规划与机器人学等AI应用领域产生重要影响。