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.