An introduction to mechanized reasoning
From MaRDI portal
Publication:504394
DOI10.1016/j.jmateco.2016.06.005zbMath1368.68289arXiv1603.02478OpenAlexW3105421491MaRDI QIDQ504394
Colin Rowat, Christoph Lange, Manfred Kerber
Publication date: 16 January 2017
Published in: Journal of Mathematical Economics (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1603.02478
Auctions, bargaining, bidding and selling, and other market models (91B26) Mechanization of proofs and logical operations (03B35) Social choice (91B14)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Equity and the Vickrey allocation rule on general preference domains
- 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
- Automated reasoning in social choice theory: some remarks
- Two equivalence results for two-person strict games
- A note on the extension of an order on a set to the power set
- Extending an order on a set to the power set: Some remarks on Kannai and Peleg's approach
- Computer-aided proofs of Arrow's and other impossibility theorems
- Formalizing Arrow's theorem
- Symbolic model checking: \(10^{20}\) states and beyond
- Every planar map is four colorable. I: Discharging
- Every planar map is four colorable. II: Reducibility
- Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
- A note on social choice theory without the Pareto principle
- Solution of the Robbins problem
- 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
- Arrow's theorem and the Gibbard-Satterthwaite theorem: A unified approach
- Three brief proofs of Arrow's impossibility theorem
- Introduction to computer science and economic theory
- Strategy-proofness versus symmetry in economies with an indivisible good and money
- Characterizing the Vickrey combinatorial auction by induction
- A proof of the Kepler conjecture
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
- Finding Strategyproof Social Choice Functions via SAT Solving
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
- Automated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects
- AfterMath: The Work of Proof in the Age of Human–Machine Collaboration
- Toward Mechanical Mathematics
- Strategy-Proofness and Pivotal Voters: A Direct Proof of the Gibbard-Satterthwaite Theorem
- Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
- Mathematical Theory Exploration
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Optimal Multi-Object Auctions
- Strategy-proofness and efficiency with non-quasi-linear preferences: A characterization of minimum price Walrasian rule
- Reducibility among Combinatorial Problems
- A Machine-Checked Proof of the Odd Order Theorem
- A Short Survey of Automated Reasoning
- A Machine-Oriented Logic Based on the Resolution Principle
- Counterexample to Euler’s conjecture on sums of like powers
- A game with no solution
- Formal Methods for Hardware Verification
- Handbook of philosophical logic. Vol. 3.
