Formalization of Wu's simple method in Coq
Abstract
We present in this paper the integration within the Coq proof assistant, of a method for automatic theorem proving in geometry. We use an approach based on the validation of a certificate. The certificate is generated by an implementation in Ocaml of a simple version of Wu's method.
Origin : Files produced by the author(s)
Loading...