Auction Theory Toolbox (ATT) – CASL

Files relevant to the CASL formalisation

  • Source repository on GitHub.
  • all-in-one ZIP archive for download
  • *.casl: CASL formalisation:
    • Vickrey.casl: Vickrey's Theorem and all of its prerequisites
  • *.hpf: proof scripts for Hets, whenever a lemma/theorem requires a multi-step proof:
    • general: consistency of all specs
    • SingleGoodAuction:
      • allocation_unique
    • Maximum:
      • only_one_maximum
    • SecondPriceAuction (with some proofs not working in the current revision, indicated by a stroke):
      • allocate_implies_spa_winner
      • not_allocated_implies_spa_loser
      • only_max_bidder_wins
      • second_price_auction_winner_payoff
      • second_price_auction_loser_payoff
      • winners_payoff_on_deviation_from_valuation
      • … and further intermediate steps: test_spa_winner_payoff_0step, test_spa_loser_payoff_0step, test_spa_winner_payoff_3step
    • VickreyPre (lots of preliminaries and intermediate steps for the weak dominance part of Vickrey's theorem; some of them proved, some open in the current revision)
    • Vickrey (preliminaries and intermediate steps for the efficiency part of Vickrey's theorem; open in the current revision)
    • Vickrey_proof (the actual proof of Vickrey's theorem; open in the current revision)
  • Shell script to run hets in the background, to experiment with long timeouts for provers
  • further relevant Makefile targets:
    • Use, e.g., make Vickrey_Maximum.tptp to export a TPTP FOF representation of the Maximum specification in Vickrey.casl. This is suitable for feeding into System on TPTP.
      Even more useful are TPTP exports of individual goals, but these you can only export interactively from the Hets GUI, by pretending to invoke a TPTP-based prover such as E for them (see below), and then saving the input file that Hets generated for sending to the prover. With Vickrey_SecondPriceAuction_only_max_bidder_wins.tptp we provide one such file for your convenience. This is known to work with E.

How to run

  1. Obtain Hets (Heterogeneous Tool Set). Our code is known to work with Hets 0.98. Hets runs on Linux and Mac OS; an image for virtual machines is available as well.
  2. Make sure that some additional tools required by Hets are installed (either via the Hets installer or by other means) and accessible in your PATH:
  3. Download the CASL libraries and set HETS_LIB to the directory where you downloaded them.
  4. Running hets -g Vickrey.casl displays the development graph GUI. In this graph, you can right-click on any theory node with open proof goals (displayed in red) and try to prove them.
  5. Some theorems cannot be proved in one step. For proving them, we provide scripts, one per theorem. You can run them with hets -I < script.hpf.

This page was last modified on 04 September 2013.