一句话：提出策略语言MuAC与逻辑MuACL，将资源交换公平性归约为逻辑证明并证明可判定。
数字平台上的资源交换需要用户声明提供与索取资源的策略，并防止恶意用户占诚实用户便宜。论文提出该环境的正式模型，定义声明式策略语言 MuAC 及其形式语义。为判定交换是否公平，作者设计非标准逻辑 MuACL，融合非线性、线性与契约式成分，证明其可判定，并指出契约蕴涵算子不可在线性逻辑中表达。随后给出保语义的编译，将 MuAC 策略转成 MuACL，从而把公平性判定归约为在 MuACL 中找证明。最后展示该方法可用于区块链上非同质化代币（NFT）的交换。
People increasingly use digital platforms to exchange resources in accordance with some policies stating what resources users offer and what they require in return. In this paper, we propose a formal model of these environments, focussing on how users' policies are defined and enforced, so ensuring that malicious users cannot take advantage of honest ones. To that end, we introduce the declarative policy language MuAC and equip it with a formal semantics. To determine if a resource exchange is fair, i.e., if it respects the MuAC policies in force, we introduce the non-standard logic MuACL that combines non-linear, linear and contractual aspects, and prove it decidable. Notably, the operator for contractual implication of MuACL is not expressible in linear logic. We define a semantics preserving compilation of MuAC policies into MuACL, thus establishing that exchange fairness is reduced to finding a proof in MuACL. Finally, we show how this approach can be put to work on a blockchain to exchange non-fungible tokens.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CeragioliDGV26,
title = {Policies for Fair Exchanges of Resources},
author = {Lorenzo Ceragioli and Pierpaolo Degano and Letterio Galletta and Luca Viganò},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 3},
year = {2026},
doi = {10.46298/lmcs-22(3:2)2026}
}