Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
EKB_GINSERT(1)			 User Commands			EKB_GINSERT(1)

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
       Copyright (C) 1999-20012	by Stephan Schulz, schulz@eprover.org

       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  MER-
       CHANTABILITY  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	 Soft-
       ware   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	Infor-
       matik Arcisstrasse 20 D-80290 Muenchen Germany

ekb_ginsert 2.0			  August 2020			EKB_GINSERT(1)

NAME | SYNOPSIS | DESCRIPTION | REPORTING BUGS | COPYRIGHT

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=ekb_ginsert&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>

home | help