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.