Unsafe mode

In order for STELF to be useful as a theorem verifier, STELF should not accept untrue or unproven assumptions. However, it is sometimes helpful for the STELF user to be able to state, and use, unproven assumptions, especially during proof development. Directives like %trustme and %assert allow the STELF user to do just this.

When STELF is set to not accept any untrue or unproven assumptions, it is in safe mode (this is the default setting). In order to use directives like %trustme, STELF must be set to unsafe mode.

Setting STELF in unsafe mode

• In STELF with Emacs, select the STELF menu, then select the Options submenu, then select the unsafe menu option.
• If using the STELF server directly from the command line, the command set unsafe true will put STELF in unsafe mode.
• In ML STELF, the SML command STELF.unsafe := true; will put STELF in unsafe mode.

See also

• Holes in metatheorems