3 papers
cs.LO2026
A Strategy Language for Controlled Proof Search
Romain Sidhoum, Simon Robillard, David Delahaye
This paper introduces the strategy language of Pgeon, a meta-prover with a clear separation between inference rules and proof search. We give the semantics of strategies as functio…
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.LO2016
Coming to Terms with Quantified Reasoning
Laura Kovacs, Simon Robillard, Andrei Voronkov
The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essentia…