coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Mandy Martino <tesleft AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] is there an example about data mining new geometry theorems with geo coq github and translate proof into a polynomials system
Date: Tue, 8 Dec 2015 18:11:45 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tesleft AT hotmail.com; spf=Pass smtp.mailfrom=tesleft AT hotmail.com; spf=None smtp.helo=postmaster AT BAY004-OMC1S16.hotmail.com
Importance: Normal
Ironport-phdr: 9a23:KTcZXh3Va2SLcegRsmDT+DRfVm0co7zxezQtwd8ZsegTIvad9pjvdHbS+e9qxAeQG96LtbQd0KGP6ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6MyZ3snLnrs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JsKWqLjOq88ULZwDTI8Mmlz6teh/U3IShLK7X8BWE0XlABJCk7L9kepcI32t37fv+xxyWG/NNfqTLYzEWC+4rxvRRH0oCcAKzsw8WWRgct12vEI6Cm9rgByltaHKLqeM+BzK/vQ

Hi,

1.would like to data mining new geometry theorems with geo coq github's coq script

is there an example script about this?

2. is there an example to translate proof into a polynomials system ?

3. would like to translate tactics proof result into type programming language, is there example about this?

4.is there any existing language can call Coq or automate Coq ? can haskell or F# or java do these?

5. how can display geometric graph with geogebra from Coq in linux and window respectively?

Regards,

Martin

[Coq-Club] is there an example about data mining new geometry theorems with geo coq github and translate proof into a polynomials system, Mandy Martino, 12/08/2015
- Re: [Coq-Club] is there an example about data mining new geometry theorems with geo coq github and translate proof into a polynomials system, Julien Narboux, 12/12/2015
  - Re: [Coq-Club] is there an example about data mining new geometry theorems with geo coq github and translate proof into a polynomials system, Martin Mandy, 12/14/2015
    - RE: [Coq-Club] is there an example about data mining new geometry theorems with geo coq github and translate proof into a polynomials system, Mandy Martino, 12/14/2015
      - Re: [Coq-Club] is there an example about data mining new geometry theorems with geo coq github and translate proof into a polynomials system, Pierre Courtieu, 12/14/2015