Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Formalise general combinatorial auctions #19

Open
clange opened this issue Sep 3, 2013 · 1 comment
Open

Formalise general combinatorial auctions #19

clange opened this issue Sep 3, 2013 · 1 comment
Assignees
@caminati
Labels
isabelle

Comments

@clange
Copy link
Member

clange commented Sep 3, 2013

In CombinatorialAuction.thy, get the formalisation of a general combinatorial auction right, including all concepts (such as what an admissible input and a well-defined outcome is; see #35 for an example of how concrete auctions could specialise these notions). Maybe prefer *_fun definitions over *_rel definitions of allocations etc., depending on what's easier to do proofs with.
@ghost ghost assigned clange Sep 3, 2013
@clange clange mentioned this issue Sep 6, 2013
Open
@ghost ghost assigned caminati Sep 6, 2013
@clange
Copy link
Member Author

clange commented Sep 11, 2013

Done for input (admissible_input, trivial in the general case) and allocation (wd_allocation). Not reasonable for payments in general.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@caminati caminati

Labels
isabelle
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@caminati @clange