The goal of this paper is to propose a framework for representing and reasoning about the rules governing a combinatorial exchange. Such a framework is at first interest as long as we want to build up digital marketplaces based on auction, a widely used mechanism for automated transactions. Combinatorial exchange is the most general case of auctions, mixing the double and combinatorial variants: agents bid to trade bundles of goods. Hence the framework should fulfill two requirements: (i) it should enable bidders to express their bids on combinations of goods and (ii) it should allow describing the rules governing some market, namely the legal bids, the allocation and payment rules. To do so, we define a logical language in the spirit of the Game Description Language: the Combinatorial Exchange Description Language is the first language for describing combinatorial exchange in a logical framework. The contribution is two-fold: first, we illustrate the general dimension by representing different kinds of protocols, and second, we show how to reason about auction properties in this machine-processable language.

翻译：本文的目的是提出一个框架,用以代表并推理关于组合式交换的规则。只要我们想在拍卖的基础上建立数字市场,这种框架就具有首要利益,因为拍卖是一种广泛使用的自动交易机制。组合式交换是拍卖的最一般例子,将双重和组合式变式混合在一起:代理商竞价进行货物捆绑交易。因此,该框架应满足两项要求:(一)它应当使投标人能够表达关于货物组合的出价,和(二)它应当允许描述某些市场的规则,即法律出价、分配和支付规则。为了这样做,我们本着“游戏描述语言:组合式交换描述语言”的精神界定了逻辑语言,这是在逻辑框架内描述组合式交换的第一语言。贡献有两个方面:第一,我们通过代表不同种类的协议来说明一般层面,第二,我们展示如何用这种机器处理的语言解释拍卖属性。