1EKB_GINSERT(1)                   User Commands                  EKB_GINSERT(1)
2
3
4

NAME

6       ekb_ginsert - manual page for ekb_ginsert 2.3-DEBUG
7

SYNOPSIS

9       ekb_ginsert [options] [name]
10

DESCRIPTION

12       ekb_ginsert 2.3-DEBUG
13
14       Generate  a  set of training examples from an E inference list (i.e. an
15       EPCL trace of a proof run) and insert it into a knowledge base.
16
17       Options
18
19       -h
20
21       --help
22
23              Print a short description of program usage and options.
24
25       -V
26
27       --version
28
29              Print the version number of the program.
30
31       -v
32
33       --verbose[=<arg>]
34
35              Verbose comments on the progress of the program. The short  form
36              or  the long form without the optional argument is equivalent to
37              --verbose=1.
38
39       -n <arg>
40
41       --name=<arg>
42
43              Give the name of the new problem. If not given, the program will
44              take the name of the first input file, or, if <stdin> is read, a
45              name of the form '__problem__i', where i is  magically  computed
46              from the existing knowledge base.
47
48       -k <arg>
49
50       --knowledge-base=<arg>
51
52              Select the knowledge base. If not given, select E_KNOWLEDGE.
53

REPORTING BUGS

55       Report  bugs  to <schulz@eprover.org>. Please include the following, if
56       possible:
57
58       * The version of the package as reported by eprover --version.
59
60       * The operating system and version.
61
62       * The exact command line that leads to the unexpected behaviour.
63
64       * A description of what you expected and what actually happend.
65
66       * If possible all input files necessary to reproduce the bug.
67

69       Copyright © 1999-20012 by Stephan Schulz, schulz@eprover.org
70
71       This program is a part of the support structure for  the  E  equational
72       theorem  prover.  You can find the latest version of the E distribution
73       as well as additional information at http://www.eprover.org
74
75       This program is free software; you can redistribute it and/or modify it
76       under  the  terms of the GNU General Public License as published by the
77       Free Software Foundation; either version 2 of the License, or (at  your
78       option) any later version.
79
80       This  program  is  distributed  in the hope that it will be useful, but
81       WITHOUT ANY  WARRANTY;  without  even  the  implied  warranty  of  MER‐
82       CHANTABILITY  or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
83       Public License for more details.
84
85       You should have received a copy of the GNU General Public License along
86       with this program (it should be contained in the top level directory of
87       the distribution in the file COPYING); if not, write to the Free  Soft‐
88       ware   Foundation,  Inc.,  59  Temple  Place,  Suite  330,  Boston,  MA
89       02111-1307 USA
90
91       The original copyright holder can be contacted as
92
93       Stephan Schulz Technische Universitaet Muenchen Fakultaet  fuer  Infor‐
94       matik Arcisstrasse 20 D-80290 Muenchen Germany
95
96
97
98ekb_ginsert 2.3-DEBUG             April 2019                    EKB_GINSERT(1)
Impressum