Twelf without Emacs

First, you should read up on STELF with Emacs, to understand how STELF programs are divided up into files and how one interacts with those files. Then, instead of using emacs, you can run the twelf-server command directly from your shell and interact with your files using the following commands. (You may find it convenient to run twelf-server under some readline wrapper program like rlwrap or ledit to get command-line editing and history.)

Loading the configuration file

To read your current config from sources.cfg, type make To read some other config other.cfg, type make other.cfg

Checking an individual declaration

To check an individual declaration, type readDecl Then, on a new line, type a STELF declaration, terminated with a period.

Checking an individual file

To load an individual file sometwelf.elf, type loadFile sometwelf.elf

Logic programming proof search

To animate your specifications by doing logic programming queries, type top You will be presented with a a prompt, ?- at which you can type queries with existential metavariables, like ?- plus (s z) (s (s z)) N. Assuming you’ve loaded the signature from the Natural numbers article), the STELF server responds with the following: Solving… N = s (s (s z)). More? You can exit the logic programming top-level by pressing Ctrl-C.

Quitting

To quit from the STELF server, type quit or press Ctrl-D.