Stålmarck's Algorithm in Coq: A Three-Level Approach
Abstract
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.
Domains
Other [cs.OH]
Loading...