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.
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
Cites work
- scientific article; zbMATH DE number 194754 (Why is no real title available?)
- scientific article; zbMATH DE number 5486212 (Why is no real title available?)
- scientific article; zbMATH DE number 3339390 (Why is no real title available?)
- scientific article; zbMATH DE number 3359806 (Why is no real title available?)
- scientific article; zbMATH DE number 3084669 (Why is no real title available?)
- scientific article; zbMATH DE number 3090127 (Why is no real title available?)
- scientific article; zbMATH DE number 3099224 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- A Short Survey of Automated Reasoning
- A game with no solution
- A machine-checked proof of the odd order theorem
- A note on Bossert, Pattanaik and Xu's ``Choice under complete uncertainty: axiomatic characterization of some decision rules
- A note on social choice theory without the Pareto principle
- A note on the extension of an order on a set to the power set
- A proof of the Kepler conjecture
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
- AfterMath: The Work of Proof in the Age of Human–Machine Collaboration
- Arrow's theorem and the Gibbard-Satterthwaite theorem: A unified approach
- Automated reasoning in social choice theory: some remarks
- Automated search for impossibility theorems in social choice theory: ranking sets of objects
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Characterizing the Vickrey combinatorial auction by induction
- Choice under complete uncertainty: Axiomatic characterizations of some decision rules
- Computer-aided proofs of Arrow's and other impossibility theorems
- Computing optimal outcomes under an expressive representation of settings with externalities
- Counterexample to Euler’s conjecture on sums of like powers
- Dense sphere packings. A blueprint for formal proofs
- Discovering theorems in game theory: two-person games with unique pure Nash equilibrium payoffs
- Equity and the Vickrey allocation rule on general preference domains
- Every planar map is four colorable. I: Discharging
- Every planar map is four colorable. II: Reducibility
- Extending an order on a set to the power set: Some remarks on Kannai and Peleg's approach
- Finding strategyproof social choice functions via SAT solving
- Formal Methods for Hardware Verification
- Formal proof - the four color theorem
- Formalizing Arrow's theorem
- Handbook of philosophical logic. Vol. 3.
- Introduction to computer science and economic theory
- Mathematical Theory Exploration
- Optimal Multi-Object Auctions
- Reducibility among combinatorial problems
- Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
- Solution of the Robbins problem
- Strategy-Proofness and Pivotal Voters: A Direct Proof of the Gibbard-Satterthwaite Theorem
- Strategy-proofness and efficiency with non-quasi-linear preferences: a characterization of minimum price Walrasian rule
- Strategy-proofness versus symmetry in economies with an indivisible good and money
- Symbolic model checking: \(10^{20}\) states and beyond
- Three brief proofs of Arrow's impossibility theorem
- Toward Mechanical Mathematics
- Two equivalence results for two-person strict games
Cited in
(9)- The ForMaRE project -- formal mathematical reasoning in economics
- scientific article; zbMATH DE number 885178 (Why is no real title available?)
- Mechanizing Logic. II: Automated map logic method for relational arguments on paper and by computer
- 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
- Economic reasoning with demand and supply graphs
- scientific article; zbMATH DE number 53302 (Why is no real title available?)
- TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics
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)
