coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ryan Wisnesky <ryan AT cs.harvard.edu>
- To: Marko Maliković <marko AT ffri.hr>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Prenex form
- Date: Mon, 3 Sep 2012 22:08:36 -0400
Such a conversion could be non-trivial in that to avoid reifying the syntax
of Prop, it would probably need to be a tactic (although you could use
explicit syntax), and regardless, it would require heavy use of a classical
logic axiom or a decidable domain. It would be pretty useful though, so I
hope it exists.
On Sep 3, 2012, at 6:20 PM, Marko Maliković
<marko AT ffri.hr>
wrote:
> Regards,
>
> Is there module for conversion first-order formulas over the Prop into
> Prenex form. I can not find it.
>
> Great thanks,
>
> -----------------------
> Dr. Sc. Marko Maliković
> Docent
> Filozofski fakultet
> Sveučilište u Rijeci
> ---------------------
> Ph.D. Marko Maliković
> Assistant Professor
> Faculty of Humanities and Social Sciences
> University of Rijeka, Croatia
> -----------------------------
> marko.malikovic AT ffri.hr
> http://www.ffri.hr/~marko
> -------------------------
- [Coq-Club] Prenex form, Marko Maliković, 09/04/2012
- Re: [Coq-Club] Prenex form, Ryan Wisnesky, 09/04/2012
- Re: [Coq-Club] Prenex form, Gregory Malecha, 09/04/2012
- Re: [Coq-Club] Prenex form, Ryan Wisnesky, 09/04/2012
- Re: [Coq-Club] Prenex form, Marko Maliković, 09/05/2012
- Re: [Coq-Club] Prenex form, Ryan Wisnesky, 09/04/2012
- Re: [Coq-Club] Prenex form, Gregory Malecha, 09/04/2012
- Re: [Coq-Club] Prenex form, Ryan Wisnesky, 09/04/2012
Archive powered by MHonArc 2.6.18.