A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

DOI10.1007/978-3-642-39320-4_13zbMath1390.68577arXiv1303.4193OpenAlexW1521892088MaRDI QIDQ2843015

Till Mossakowski, Makarius Wenzel, Wolfgang Windsteiger, Colin Rowat, Manfred Kerber, Christoph Lange, Marco Bright Caminati

Publication date: 9 August 2013

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1303.4193

Mathematics Subject Classification ID

Auctions, bargaining, bidding and selling, and other market models (91B26) Software, source code, etc. for problems pertaining to game theory, economics, and finance (91-04)

Related Items (4)

The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema ⋮ Recycling proof patterns in Coq: case studies ⋮ An introduction to mechanized reasoning ⋮ Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?

Uses Software

• Isabelle
• Theorema
• Isabelle/HOL
• MizarMode
• CASL
• PVS
• TPTP
• Mizar
• Isabelle/jEdit
• Hets

This page was built for publication: A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory