*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Proving consistency*From*: John Munroe <munddr at gmail.com>*Date*: Thu, 19 Aug 2010 15:50:43 +0100

Hi all, I was wondering how consistency can be proved in general. For example, for the following simple setup: locale A = fixes a :: real and b :: real assumes ax1: "a > 0 & b > 0" and ax2: "a + b > 0" What is the theorem for proving that A is consistent? On paper, I'd like to show that I can't prove False from A, but how can that be done in practice? Thank you in advance, John

**Follow-Ups**:**Re: [isabelle] Proving consistency***From:*Benedikt N

**Re: [isabelle] Proving consistency***From:*Tjark Weber

- Previous by Date: Re: [isabelle] classes and interpretations
- Next by Date: Re: [isabelle] stuck on proof
- Previous by Thread: Re: [isabelle] classes and interpretations
- Next by Thread: Re: [isabelle] Proving consistency
- Cl-isabelle-users August 2010 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