ekb_ginsert1

Usage

Overview

ekb_ginsert 3.2.5

Generate a set of training examples from an E inference list (i.e. an EPCL trace of a proof run) and insert it into a knowledge base.

Options

-h

--help

Print a short description of program usage and options.

-V

--version

Print the version number of the program.

-v

--verbose[=<arg>]

Verbose comments on the progress of the program. The short form or the long form without the optional argument is equivalent to --verbose=1.

-n <arg>

--name=<arg>

Give the name of the new problem. If not given, the program will take the name of the first input file, or, if <stdin> is read, a name of the form '__problem__i', where i is magically computed from the existing knowledge base.

-k <arg>

--knowledge-base=<arg>

Select the knowledge base. If not given, select E_KNOWLEDGE.