In systems modelling, a system typically comprises located resources relative to which processes execute. One important use of logic in informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a resource semantics of the logic. This paper shows how inferentialism -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components.
翻译:在系统建模中,系统通常包含与进程执行相关的定位资源。逻辑学在信息学中的一个重要应用是对此类系统进行建模,以推理(可能通过自动化方式)其行为与性质。为此,需要根据系统资源与状态对逻辑公式进行解释;此类解释被称为逻辑的资源语义学。本文展示了推理主义(即认为意义由推理行为赋予的观点)如何为资源语义学构建一个灵活且富有表达力的框架。具体而言,推理主义如何无缝整合了束蕴含逻辑(Bunched Implications)中基于断言的路径(该路径是程序验证的基础,例如作为分离逻辑的基础),以及线性逻辑(Linear Logic)中著名的"使用次数"解读。这种整合使得我们能够以直观且熟悉的方式对共享资源和分离资源进行推理,同时对系统组件的组合与接口进行推理。