Logical Foundations of Resource

*资源问题*在计算机科学和现实世界中普遍存在；事实上，计算的基本概念与资源（时间、内存等）的概念有着千丝万缕的联系。逻辑为资源属性的表达和推理提供了一种强大而方便的方法，过去已经提出了各种面向资源的逻辑。可以说，迄今为止基于逻辑的资源推理最成功的应用是使用基于“聚束逻辑”的“分离逻辑”及其相关逻辑来验证内存操作和并发计算机程序。然而，所采用的技术高度专门化于验证问题的许多领域特定属性；因此，它们不会直接转移到其他域。虽然前面提到的进展是重要的，但我们建议，面向资源的逻辑可以用于对资源问题进行更广泛和一致的攻击，这与资源在广泛的应用程序领域中的中心作用是一致的。这将通过提供统一的基础资源概念并使用这些概念开发新的应用程序来实现。我们的计划是将资源推理引入两个主要的新方向。第一个方向是对资源本身采取更一般的看法。例如，可以考虑“二元”资源（例如金融投资组合中的资产和负债）或可以以几种不同方式组装的资源（很像乐高积木）。第二个方向是不仅要考虑验证，还要考虑各种其他实际资源问题，包括资源分配、调度、绑架和计划。这与许多领域中出现的资源问题的方式相对应，但到目前为止，资源逻辑几乎没有解决这些问题。我们提出，通过使用合适的资源逻辑来表达资源属性，以上所有的资源问题实际上都可以本质上重新定义为“证明搜索”问题。这种方法有可能显著地统一这些不同的资源问题，并为解决这些问题的符号方法开辟了道路，这可能导致更具可扩展性的解决方案（例如，符号模型检查）。解决这些证明搜索问题需要相当复杂的搜索算法，因为搜索空间可能太大，无法进行详尽的探索。我们计划采用自动化定理证明技术，以及用于面向智能体计算的强化学习技术。通过将这些技术与基于资源逻辑的符号方法相结合，我们的目标是开发既强大又可广泛转移的形式化方法。如果这个建议达到了它的研究目标，那么我们期望对资源分配、规划和其他相关资源问题的处理方式产生重大影响。这些问题不仅是计算机科学及其各个子领域（如分布式系统、面向代理的计算和人工智能）的基础，也是经济学、工程学、环境科学和金融等其他领域的基础，也是英国软件、电子、公用事业供应、运输和制造业等行业的基础。

*Resource problems* are pervasive in computer science and the real world; indeed, the fundamental concept of computation is inextricably linked with the concept of resource (time, memory, etc.). Logic provides a powerful andconvenient method for expressing and reasoning about properties of resource, and various resource-oriented logics have been advanced for this purpose in the past. Arguably the most successful application of logic-based resourcereasoning to date is the use of *separation logic* and its relatives, based on *bunched logic*, to verify memory-manipulating and concurrent computer programs. The techniques employed are, however, highly specialised to the many domain-specific properties of the verification problem; thus they do not straightforwardly transfer to other domains.While the aforementioned advances are significant, we propose that resource-oriented logics can be used to stage a much more wide-ranging and coherent attack on resource problems in general, in line with the central role of resource in a very broad spectrum of application domains. This will be achieved by providing unifying, foundational resource concepts and using these concepts to develop novel applications.Our plan is to take resource reasoning in two main new directions. The first direction is to take a much more general view of resources themselves. For example, one can consider resources which *dualise* (e.g. assets andliabilities in a financial portfolio) or which can be assembled in several different ways (much like LEGO construction bricks). The second direction is to consider not just verification but a variety of other practical resourceproblems, including resource allocation, scheduling, abduction and planning. These correspond to the way that resource problems arise in a number of fields, but have until now been little addressed by resource logics.We propose that, using suitable resource logics to express resource properties, all of the resource problems above can in fact be recast essentially as *proof search* problems. Such an approach has the potential to significantly unify these diverse resource problems, and open the way for symbolic approaches to them, which could lead to more scalable solutions (as in, e.g., symbolic model checking). Solving these proof search problems will then require search algorithms of considerable sophistication, since the search space may be far too large to explore exhaustively. We plan to employtechniques from automated theorem proving, and from reinforcement learning as used in agent-oriented computing. By combining these techniques with our symbolic methods based upon resource logics, we aim to develop formal methodsthat are both powerful and widely transferable.If this proposal achieves its research aims then we expect a significant impact on the way that resource allocation, planning and other related resource problems are handled. These problems are fundamental not only tocomputer science and its various subfields (e.g. distributed systems, agent-oriented computing, and artificial intelligence) but also to other fields such as economics, engineering, environmental science and finance, andto UK industries such as software, electronics, utility provision, transportation and manufacturing.