default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDArchive of Formal Proofs, Volume 2025
Volume 2025, 2025
- Christoph Benzmüller, Dana S. Scott:
Notes on Gödel's and Scott's Variants of the Ontological Argument (Isabelle/HOL dataset). - Emin Karayel:
Negatively Associated Random Variables. - Louis Cheung, Christine Rizkallah:
Formalised Burrows-Wheeler Transform. - Katherine Kosaian, Zili Wang, Elizabeth Sloan:
Mission-time Linear Temporal Logic. - Zili Wang, Katherine Kosaian:
Mission-time Linear Temporal Logic to Regular Expressions. - Tetsuya Sato, Yasuhiko Minamide:
Differential Privacy. - Michikazu Hirata:
Differential Privacy using Quasi-Borel Spaces. - Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Transitive Union-Closed Families. - Pablo Manrique:
Quantum Fourier Transform. - Stepan Holub, Martin Raska, Stepán Starosta, Tobias Nipkow:
Power Operator for Lists. - Dmitriy Traytel:
Formalization of (Conflict-)Serializability and Strict Two-Phase Locking. - Emin Karayel, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan, Seng Joe Watt:
Verification of the CVM algorithm with a New Recursive Analysis Technique. - Benjamin Puyobro, Benoît Ballenghien, Burkhart Wolff:
A Proof of Hilbert Basis Theorem and an Extension to Formal Power Series. - Sophie Tourret, Lawrence C. Paulson:
Compactness Theorem for First-Order Logic. - Mohammad Abdulaziz:
Elementary Graph Traversal Algorithms. - Balázs Tóth:
First Order Clause. - Zili Wang, Katherine Kosaian, Alec Rosentrater:
Language Partitioning for Mission-time Linear Temporal Logic. - Benjamin Puyobro:
Morley's Theorem. - Vivek Soorya Maadoori, Syed Mohammad Meesum, Shiv Pillai, T. V. H. Prathamesh, Aditya Swami:
Formal Proof of Dilworth's Theorem. - Filip Maric, Jelena Markovic:
Formalization of Gyrovector Spaces as Models of Hyperbolic Geometry and Special Relativity. - Christian Pardillo Laursen, Simon Foster:
The Kolmogorov-Chentsov theorem. - Benoît Ballenghien:
Sophie Germain's Theorem. - Benoît Ballenghien, Benjamin Puyobro, Burkhart Wolff:
Definition and Elementary Properties of Ultrametric Spaces. - Ievgen Ivanov:
Completeness of Decreasing Diagrams for the Least Uncountable Cardinality. - René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler, Akihisa Yamada:
First-Order Rewriting. - Christina Kirk:
Proof Terms for Term Rewriting. - Yiran Duan, Lukas Stevens:
A Verified Reduction Algorithm from MLSSmf to MLSS. - Christoph Benzmüller:
Faithful Logic Embeddings in HOL - Deep and Shallow (Isabelle/HOL dataset). - Benoît Ballenghien, Burkhart Wolff:
CSP Semantics over Restriction Spaces. - Benoît Ballenghien, Benjamin Puyobro, Burkhart Wolff:
Restriction Spaces: a Fixed-Point Theory. - Benoît Ballenghien, Benjamin Puyobro, Burkhart Wolff:
Examples of Restriction Spaces. - Benoît Ballenghien, Benjamin Puyobro, Burkhart Wolff:
Ultrametric Structure for Restriction Spaces. - Lawrence C. Paulson:
Farey Sequences and Ford Circles. - Simon Foster:
Shallow Expressions. - Tobias Nipkow, Markus Gschoßmann, Felix Krayer, Fabian Lehr, Bruno Philipp, August Martin Stimpfle, Kaan Taskin, Akihisa Yamada:
Context-Free Grammars and Languages. - Simon Wimmer:
Munta: A Verified Model Checker for Timed Automata.
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 2025-07-06 18:30 CEST 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:
