An introduction to mechanized reasoning (Q504394): Difference between revisions

@@ Property / describes a project that uses @@
+kepler98
@@ Property / describes a project that uses: kepler98 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Arrow Gibbard Satterthwaite
@@ Property / describes a project that uses: Arrow Gibbard Satterthwaite / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3105421491
@@ Property / OpenAlex ID: W3105421491 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.02478
@@ Property / arXiv ID: 1603.02478 / rank @@
+Normal rank
@@ Property / cites work @@
+Equity and the Vickrey allocation rule on general preference domains
+Normal rank
@@ Property / cites work @@
+Every planar map is four colorable. I: Discharging
+Normal rank
@@ Property / cites work @@
+Every planar map is four colorable. II: Reducibility
+Normal rank
@@ Property / cites work @@
+A note on Bossert, Pattanaik and Xu's ``Choice under complete uncertainty: axiomatic characterization of some decision rules''
+Normal rank
@@ Property / cites work @@
+Optimal Multi-Object Auctions
@@ Property / cites work: Optimal Multi-Object Auctions / rank @@
+Normal rank
@@ Property / cites work @@
+Strategy-Proofness and Pivotal Voters: A Direct Proof of the Gibbard-Satterthwaite Theorem
+Normal rank
@@ Property / cites work @@
+Extending an order on a set to the power set: Some remarks on Kannai and Peleg's approach
+Normal rank
@@ Property / cites work @@
+Introduction to computer science and economic theory
+Normal rank
@@ Property / cites work @@
+Choice under complete uncertainty: Axiomatic characterizations of some decision rules
+Normal rank
@@ Property / cites work @@
+Finding Strategyproof Social Choice Functions via SAT Solving
+Normal rank
@@ Property / cites work @@
+Mathematical Theory Exploration
@@ Property / cites work: Mathematical Theory Exploration / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic model checking: \(10^{20}\) states and beyond
+Normal rank
@@ Property / cites work @@
+Automated reasoning in social choice theory: some remarks
+Normal rank
@@ Property / cites work @@
+Characterizing the Vickrey combinatorial auction by induction
+Normal rank
@@ Property / cites work @@
+Automatic verification of finite-state concurrent systems using temporal logic specifications
+Normal rank
@@ Property / cites work @@
+Computing optimal outcomes under an expressive representation of settings with externalities
+Normal rank
@@ Property / cites work @@
+Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
+Normal rank
@@ Property / cites work @@
+AfterMath: The Work of Proof in the Age of Human–Machine Collaboration
+Normal rank
@@ Property / cites work @@
+Handbook of philosophical logic. Vol. 3.
@@ Property / cites work: Handbook of philosophical logic. Vol. 3. / rank @@
+Normal rank
@@ Property / cites work @@
+Three brief proofs of Arrow's impossibility theorem
+Normal rank
@@ Property / cites work @@
+Automated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects
+Normal rank
@@ Property / cites work @@
+Q5302559
@@ Property / cites work: Q5302559 / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+A proof of the Kepler conjecture
@@ Property / cites work: A proof of the Kepler conjecture / rank @@
+Normal rank
@@ Property / cites work @@
+Q2892718
@@ Property / cites work: Q2892718 / rank @@
+Normal rank
@@ Property / cites work @@
+A Short Survey of Automated Reasoning
@@ Property / cites work: A Short Survey of Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods for Hardware Verification
@@ Property / cites work: Formal Methods for Hardware Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q5616133
@@ Property / cites work: Q5616133 / rank @@
+Normal rank
@@ Property / cites work @@
+A note on the extension of an order on a set to the power set
+Normal rank
@@ Property / cites work @@
+Reducibility among Combinatorial Problems
@@ Property / cites work: Reducibility among Combinatorial Problems / rank @@
+Normal rank
@@ Property / cites work @@
+Strategy-proofness versus symmetry in economies with an indivisible good and money
+Normal rank
@@ Property / cites work @@
+Counterexample to Euler’s conjecture on sums of like powers
+Normal rank
@@ Property / cites work @@
+A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
+Normal rank
@@ Property / cites work @@
+A game with no solution
@@ Property / cites work: A game with no solution / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692751
@@ Property / cites work: Q4692751 / rank @@
+Normal rank
@@ Property / cites work @@
+A note on social choice theory without the Pareto principle
+Normal rank
@@ Property / cites work @@
+Q5633670
@@ Property / cites work: Q5633670 / rank @@
+Normal rank
@@ Property / cites work @@
+Solution of the Robbins problem
@@ Property / cites work: Solution of the Robbins problem / rank @@
+Normal rank
@@ Property / cites work @@
+Strategy-proofness and efficiency with non-quasi-linear preferences: A characterization of minimum price Walrasian rule
+Normal rank
@@ Property / cites work @@
+Q5821521
@@ Property / cites work: Q5821521 / rank @@
+Normal rank
@@ Property / cites work @@
+Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
+Normal rank
@@ Property / cites work @@
+Q5839903
@@ Property / cites work: Q5839903 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5828993
@@ Property / cites work: Q5828993 / rank @@
+Normal rank
@@ Property / cites work @@
+Arrow's theorem and the Gibbard-Satterthwaite theorem: A unified approach
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
+Normal rank
@@ Property / cites work @@
+Computer-aided proofs of Arrow's and other impossibility theorems
+Normal rank
@@ Property / cites work @@
+Discovering theorems in game theory: two-person games with unique pure Nash equilibrium payoffs
+Normal rank
@@ Property / cites work @@
+Two equivalence results for two-person strict games
+Normal rank
@@ Property / cites work @@
+Toward Mechanical Mathematics
@@ Property / cites work: Toward Mechanical Mathematics / rank @@
+Normal rank
@@ Property / cites work @@
+Q5302561
@@ Property / cites work: Q5302561 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Arrow's theorem
@@ Property / cites work: Formalizing Arrow's theorem / rank @@
+Normal rank
@@ Property / cites work @@
+A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
+Normal rank