Stålmarck's Algorithm in Coq: A Three-Level Approach
Résumé
One of the most efficient method to check if a boolean proposition is a tautology is Stålmarck's algorithm. This paper reports on some experiments in integrating this algorithm inside the Coq theorem prover in a safe way.
Domaines
Autre [cs.OH]
Loading...