Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Prenex form

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prenex form


Chronological Thread 
  • 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
> -------------------------




Archive powered by MHonArc 2.6.18.

Top of Page