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逻辑(程序验证的基础,例如作为分离逻辑的基础)的基于断言的方法,以及线性逻辑著名的使用次数解读。这种整合使得能够以直观且熟悉的方式推理共享和分离的资源,以及系统组件的组合与接口。