*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] A general TP/logic question*From*: John Munroe <munddr at gmail.com>*Date*: Wed, 23 Mar 2011 15:31:30 +0000

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

**Follow-Ups**:**Re: [isabelle] A general TP/logic question***From:*Mark.Janney

**Re: [isabelle] A general TP/logic question***From:*John Thingstad

- Previous by Date: Re: [isabelle] real_vector
- Next by Date: Re: [isabelle] A general TP/logic question
- Previous by Thread: Re: [isabelle] real_vector
- Next by Thread: Re: [isabelle] A general TP/logic question
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list