The fair division literature in economics considers how to divide resources between multiple agents such that the allocation is envy-free: each agent receives their favorite piece. Researchers have developed a variety of fair division protocols for the most standard setting, where the agents want to split a single item, however, the protocols are highly intricate and the proofs of envy-freeness involve tedious case analysis. We propose Slice, a domain specific language for fair-division. Programs in our language can be converted to logical formulas encoding envy-freeness and other target properties. Then, the constraints can be dispatched to automated solvers. We prove that our constraint generation procedure is sound and complete. We also report on a prototype implementation of Slice, which we have used to automatically check envy-freeness for several protocols from the fair division literature.

翻译：经济学中的公平分配文献探讨如何在多个参与者间分配资源，使得分配结果无嫉妒：每位参与者都能获得其偏好的部分。研究人员针对最标准的场景（参与者希望分割单一物品）开发了多种公平分配协议，然而这些协议极为繁琐，且无嫉妒性的证明需要处理冗长的案例分情况讨论。我们提出Slice，一种面向公平分配的领域特定语言。基于该语言编写的程序可转换为编码无嫉妒性及其他目标属性的逻辑公式，进而将约束条件提交给自动化求解器处理。我们证明了该约束生成过程是可靠且完备的。本文还报告了Slice原型实现的开发情况，已利用该实现自动验证了公平分配文献中多个协议的无嫉妒性。