Previous Up Next

4  The h1 Prover

Most of the features of h1 are explained in Section 3. We explain the structure of the h1 command line in Section 4.1, then turn to the theoretical basis of h1 in Section 4.2. We refine this description in Section 4.3, by stating the precise rules used by h1.

4.1  How to Use h1

The h1 tool recognizes the following options. As in all Unix tools, options start with a minus sign -. Some options are flags, which can be toggled between an active state and a deactivated state. In this case, the convention used in h1 and other tools of the h1 suite is to have -<option> activate the option, while -no-<option> deactivates it.

The options recognized by the h1 prover are:

4.2  Theoretical Background

The essentials of the algorithmic underpinnings of h1 are described, rather tersely, in [2005  (Goubault-Larrecq)]: h1 implements a form of ordered resolution with selection

4.3  Principle of Operation

Previous Up Next