BLESS 3.2.3 works fine with OSATE v2.13.0-final

12 views

Skip to first unread message

Brian Larson

unread,

Jan 28, 2024, 12:03:03 AM1/28/24

to OSATE

I don't know what I did to fix the missing injector provider issue, but the current build of BLESS (v3.2.3) works fine with OSATE v2.13.0.

BLESS v3.2.3 adds references to Metamath (math about math) soundness proofs for the axioms and inference rules used to transform programs having proof outlines into deductive proofs.

A new version of the "BLESS Book" containing all the refernced theorems will be available shortly on multitude.net.

For those who encounter problems with injector providers like those in topic "BLESS 3.2.2 does not . . .", I wish I had suggestions how to fix your problem, but I don't.