NAME

ekb_ginsert - manual page for ekb_ginsert 2.0

SYNOPSIS

ekb_ginsert [options] [name]

DESCRIPTION

ekb_ginsert 2.0

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.

REPORTING BUGS

Report bugs to <schulz@eprover.org>. Please include the following, if possible:

* The version of the package as reported by eprover --version.

* The operating system and version.

* The exact command line that leads to the unexpected behaviour.

* A description of what you expected and what actually happend.

* If possible all input files necessary to reproduce the bug.

COPYRIGHT

This program is a part of the support structure for the E equational theorem prover. You can find the latest version of the E distribution as well as additional information at http://www.eprover.org

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program (it should be contained in the top level directory of the distribution in the file COPYING); if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

The original copyright holder can be contacted as

Stephan Schulz Technische Universitaet Muenchen Fakultaet fuer Informatik Arcisstrasse 20 D-80290 Muenchen Germany