default search action
Archive of Formal Proofs, Volume 2022
Volume 2022, 2022
- Lukas Koller:
Knight's Tour Revisited Revisited. - Lawrence C. Paulson:
Irrational numbers from THE BOOK. - Yosuke Ito:
Actuarial Mathematics. - Emin Karayel:
Median Method. - Emin Karayel:
Interpolation Polynomials (in HOL-Algebra). - Asta Halkjær From, Frederik Krogsdal Jacobsen:
A Sequent Calculus Prover for First-Order Logic with Functions. - Lawrence C. Paulson:
Young's Inequality for Increasing Functions. - Alexander Lochmann, Bertram Felgenhauer:
First-Order Theory of Rewriting. - René Thiemann:
Duality of Linear Programming. - Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato:
Quasi-Borel Spaces. - Emin Karayel:
Enumeration of Equivalence Relations. - Martin Raszyk:
Multi-Head Monitoring of Metric Dynamic Logic. - Martin Raszyk:
First-Order Query Evaluation. - Lawrence C. Paulson:
Wetzel's Problem and the Continuum Hypothesis. - Emin Karayel:
Universal Hash Families. - Eugene W. Stark:
Residuated Transition Systems. - Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg:
Transitive Models of Fragments of ZFC. - Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg:
The Independence of the Continuum Hypothesis in Isabelle/ZF. - Manuel Eberl:
A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent. - Asta Halkjær From:
A Naive Prover for First-Order Logic. - Lawrence C. Paulson:
Ackermann's Function Is Not Primitive Recursive. - Jacques D. Fleuriot, Lawrence C. Paulson:
Constructing the Reals as Dedekind Cuts of Rationals. - Emin Karayel:
Formalization of Randomized Approximation Algorithms for Frequency Moments. - Emin Karayel:
A Combinator Library for Prefix-Free Codes. - René Thiemann, Lukas Schmidinger:
The Generalized Multiset Ordering is NP-Complete. - Manuel Eberl:
The Sophomore's Dream. - Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock:
Digit Expansions. - Chelsea Edmonds, Lawrence C. Paulson:
Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics. - René Thiemann:
Clique is not solvable by monotone circuits of polynomial size. - Thibault Dardinier:
Formalization of a Framework for the Sound Automation of Magic Wands. - Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
The Plünnecke-Ruzsa Inequality. - Thibault Dardinier:
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand. - Alexander Lochmann:
Reducing Rewrite Properties to Properties on Ground Terms. - Jonas Bayer, Marco David, Benedikt Stock, Abhik Pal, Yuri V. Matiyasevich, Dierk Schleicher:
Diophantine Equations and the DPRM Theorem. - Emin Karayel:
Finite Fields. - Tobias Klenze, Christoph Sprenger
:
IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols. - Jeffrey Ketland:
Boolos's Curious Inference in Isabelle/HOL. - Balázs Tóth, Tobias Nipkow:
Real-Time Double-Ended Queue. - Pasquale Noce:
A Reuse-Based Multi-Stage Compiler Verification for Language IMP. - Manuel Eberl:
Pólya's Proof of the Weighted Arithmetic-Geometric Mean Inequality. - Diego Marmsoler, Achim D. Brucker:
Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL. - Mnacho Echenim:
Simultaneous diagonalization of pairwise commuting Hermitian matrices. - Achim D. Brucker:
Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML. - Robert Sachtleben:
Verified Complete Test Strategies for Finite State Machines. - Maksym Bortin:
From THE BOOK: Two Squares via Involutions. - Stephan Merz, Vincent Trélat:
Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph. - Thomas Ammer, Katharina Kreuzer:
Number Theoretic Transform. - Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Khovanskii's Theorem. - Ujkan Sulejmani, Manuel Eberl, Katharina Kreuzer:
The Hales-Jewett Theorem. - Thibault Dardinier:
Unbounded Separation Logic. - Katharina Kreuzer:
CRYSTALS-Kyber. - Asta Halkjær From, Jørgen Villadsen:
Soundness and Completeness of Implicational Logic. - Matthew Doty:
Risk-Free Lending. - Aaron Crighton:
p-adic Fields and p-adic Semialgebraic Sets. - Laura P. Gamboa Guzman:
Stalnaker's Epistemic Logic. - Martin Raszyk, Dmitriy Traytel:
Making Arbitrary Relational Calculus Queries Safe-Range. - Nils Cremer:
Maximum Segment Sum. - Chelsea Edmonds:
Undirected Graph Theory. - Lukas Stevens, Bernhard Stöckl:
Verification of Query Optimization Algorithms. - Théo Delemazure, Tom Demeulemeester, Manuel Eberl, Jonas Israel, Patrick Lederer:
The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections. - Paul Hofmeier, Emin Karayel:
Combinatorial Enumeration Algorithms. - Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds:
The Balog-Szemerédi-Gowers Theorem. - Nils Lauermann:
Turán's Graph Theorem. - Mantas Baksys, Angeliki Koutsoukou-Argyraki:
Kneser's Theorem and the Cauchy-Davenport Theorem. - Ata Keskin:
Sauer-Shelah Lemma. - Seung Hoon Park:
A Formal CHERI-C Memory Model. - Christian Dalvit, René Thiemann:
A Verified Translation of Multitape Turing Machines into Singletape Turing Machines. - Matthew Doty:
Birkhoff's Representation Theorem For Finite Distributive Lattices. - Daniel Kirchner:
Abstract Object Theory. - Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe:
Automation of Boolos' Curious Inference in Isabelle/HOL. - Katherine Cordwell, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. - Matthew Doty:
Class-based Classical Propositional Logic.
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-15 19:21 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: