# Re: [isabelle] A general TP/logic question

Yes it makes sense.. In stead of me going into detail I suggest you read
the short document the link points to.
www.cs.umd.edu/~gasarch/largeramsey/bovINTRO.pdf
> Hi,
>
> I have a general theorem proving/logic question: does it make sense to
> have a proof obligation that checks for unprovability? For example,
> the proof obligation may require that a particular sentence, like "f =
> g" to be unprovable from a theory T, i.e. "T |+ f = g". Checking for
> unprovability is undecidable, right? If such a constraint is
> impractical, then is there a more practical formulation for checking
> the same/similar property?
>
> Thanks a lot
> John
>
>

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*