An introduction to mechanized reasoning
From MaRDI portal
Publication:504394
DOI10.1016/J.JMATECO.2016.06.005zbMATH Open1368.68289arXiv1603.02478OpenAlexW3105421491MaRDI QIDQ504394FDOQ504394
Authors: Manfred Kerber, Christoph Lange, Colin Rowat 
Publication date: 16 January 2017
Published in: Journal of Mathematical Economics (Search for Journal in Brave)
Abstract: Mechanized reasoning uses computers to verify proofs and to help discover new theorems. Computer scientists have applied mechanized reasoning to economic problems but -- to date -- this work has not yet been properly presented in economics journals. We introduce mechanized reasoning to economists in three ways. First, we introduce mechanized reasoning in general, describing both the techniques and their successful applications. Second, we explain how mechanized reasoning has been applied to economic problems, concentrating on the two domains that have attracted the most attention: social choice theory and auction theory. Finally, we present a detailed example of mechanized reasoning in practice by means of a proof of Vickrey's familiar theorem on second-price auctions.
Full work available at URL: https://arxiv.org/abs/1603.02478
Recommendations
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- Automated reasoning in social choice theory: some remarks
- Computer-aided verification for mechanism design
- Formalizing Arrow's theorem
- Automated mechanism design: a new application area for search algorithms
Social choice (91B14) Auctions, bargaining, bidding and selling, and other market models (91B26) Mechanization of proofs and logical operations (03B35)
Cites Work
- Dense sphere packings. A blueprint for formal proofs
- A proof of the Kepler conjecture
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Title not available (Why is that?)
- Reducibility among combinatorial problems
- Title not available (Why is that?)
- Symbolic model checking: \(10^{20}\) states and beyond
- Every planar map is four colorable. I: Discharging
- Every planar map is four colorable. II: Reducibility
- Title not available (Why is that?)
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- A Machine-Oriented Logic Based on the Resolution Principle
- Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
- Solution of the Robbins problem
- Formal proof - the four color theorem
- Title not available (Why is that?)
- Arrow's theorem and the Gibbard-Satterthwaite theorem: A unified approach
- Three brief proofs of Arrow's impossibility theorem
- Strategy-proofness and efficiency with non-quasi-linear preferences: a characterization of minimum price Walrasian rule
- A note on Bossert, Pattanaik and Xu's ``Choice under complete uncertainty: axiomatic characterization of some decision rules
- Choice under complete uncertainty: Axiomatic characterizations of some decision rules
- Optimal Multi-Object Auctions
- Extending an order on a set to the power set: Some remarks on Kannai and Peleg's approach
- A note on social choice theory without the Pareto principle
- A game with no solution
- Automated search for impossibility theorems in social choice theory: ranking sets of objects
- Computer-aided proofs of Arrow's and other impossibility theorems
- Strategy-Proofness and Pivotal Voters: A Direct Proof of the Gibbard-Satterthwaite Theorem
- Title not available (Why is that?)
- A note on the extension of an order on a set to the power set
- Characterizing the Vickrey combinatorial auction by induction
- Equity and the Vickrey allocation rule on general preference domains
- Toward Mechanical Mathematics
- Computing optimal outcomes under an expressive representation of settings with externalities
- Discovering theorems in game theory: two-person games with unique pure Nash equilibrium payoffs
- Two equivalence results for two-person strict games
- Title not available (Why is that?)
- Formal Methods for Hardware Verification
- Formalizing Arrow's theorem
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- Automated reasoning in social choice theory: some remarks
- A machine-checked proof of the odd order theorem
- A Short Survey of Automated Reasoning
- Introduction to computer science and economic theory
- Strategy-proofness versus symmetry in economies with an indivisible good and money
- Finding strategyproof social choice functions via SAT solving
- AfterMath: The Work of Proof in the Age of Human–Machine Collaboration
- Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
- Mathematical Theory Exploration
- Title not available (Why is that?)
- Counterexample to Euler’s conjecture on sums of like powers
- Handbook of philosophical logic. Vol. 3.
Cited In (9)
- Machines Reasoning About Machines: 2015
- Computer-aided verification for mechanism design
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
- The ForMaRE project -- formal mathematical reasoning in economics
- Title not available (Why is that?)
- Mechanizing Logic. II: Automated map logic method for relational arguments on paper and by computer
- Title not available (Why is that?)
- Economic reasoning with demand and supply graphs
- TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics
Uses Software
This page was built for publication: An introduction to mechanized reasoning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q504394)
