The Coq mailing list

["Marko Maliković" <marko AT ffri.hr>]

Regards and thanks to Gregory and Ryan,

I understand that there are theoretical problems. But I'm interested in
formulae built from terms of the LIA and universal and existential
quantifiers and propositional connectives. So, over Prop. There exists
standard algorithms for this. I was interested whether the implementation
of such a conversion exists in Coq.
So, I will conclude that there is not such implementation in Coq and that
I have to develop alone for my needs (as a tactic or as a Ltac function -
nevertheless).

Thanks again and greetings,

Marko Malikovic

> Another issue: in addition to excluded middle, FOL and its prenex
> conversion assumes a non-empty domain of discourse and there are empty Coq
> types.
>
> On Sep 4, 2012, at 10:00 AM, Gregory Malecha 
> <gmalecha AT eecs.harvard.edu>
> wrote:
>
>> Hi --
>>
>> Is this guaranteed when you have dependent types? You could try to pull
>> apart the dependency, but it isn't clear to me that it is always
>> possible.
>>
>> Inductive IsEven : nat -> Type :=
>> | Pf : forall n, Even n -> IsEven n.
>>
>> forall x : nat, Even x -> exists y : IsEven x, True
>>
>> What would be the prenex form for this? You can't move the existential
>> before the "Even x". It seems like you would need a way to pull
>> dependency out of values, or treat -> as forall (does that defeat the
>> purpose? I don't know).
>>
>>
>> On Mon, Sep 3, 2012 at 10:08 PM, Ryan Wisnesky 
>> <ryan AT cs.harvard.edu>
>> wrote:
>> 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
>> > -------------------------
>>
>>
>>
>> --
>> gregory malecha
>> http://www.people.fas.harvard.edu/~gmalecha/