--- layout: fc_discuss_archives title: Message 86 from Frama-C-discuss on May 2010 ---
Boris Hollas wrote: > On Thu, 2010-05-20 at 15:30 +0200, Virgile Prevosto wrote: > >> No, jessie always generates a proof obligation corresponding to the >> lemma. However, no automated prover will be able to discharge it >> (otherwise, they would prove the PO from the ensures clause directly). >> Thus, some additional work is needed (e.g. by using the coq output of >> why). >> > > I don't understand that why no automatic prover will be able to prove a > user-supplied lemma. Isn't this what SMT provers are supposed to do? > I thought that a lemma is a way to reduce the search space for the > prover by giving it a hint on how to prove the postcondition. > > Indeed, you are right and Virgile is not: It is possible that a prover proves both the lemma and the assertion which need that lemma, but does not prove the assertion without the lemma. So yes, a lemma may act as an hint. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |