9 citations · 22 across the 10 of their papers we have counts for
Showing 2021Show all
3 papers · 1 filter
cs.LO2021★ 7 cited
Isabelle's Metalogic: Formalization and Proof Checker
Tobias Nipkow, Simon Roßkopf
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogi…
cs.LO2021
Verified Approximation Algorithms
Robin Eßmann, Tobias Nipkow, Simon Robillard +1
We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balanci…
cs.LO2021★ 4 cited
A Verified Decision Procedure for Orders in Isabelle/HOL
Lukas Stevens, Tobias Nipkow
We present the first verified implementation of a decision procedure for the quantifier-free theory of partial and linear orders. We formalise the procedure in Isabelle/HOL and pro…