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.

> 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.