research
∙
02/27/2023
Reimplementing Mizar in Rust
This paper describes a new open-source proof processing tool, mizar-rs, ...
share
research
∙
09/20/2021
A Flexible Proof Format for SAT Solver-Elaborator Communication
We introduce FRAT, a new proof format for unsatisfiable SAT problems, an...
research
∙
10/22/2019
Metamath Zero: The Cartesian Theorem Prover
As the usage of theorem prover technology expands, so too does the relia...
research
∙
07/02/2019
Specifying verified x86 software from scratch
We present a simple framework for specifying and proving facts about the...
research
∙
10/19/2018