How to run gkc on the Wordnet TPTP version

• Preliminary: get the latest release of gkc from gkc releases (currently delta) and either download a binary or compile using instructions on the gkc github page.

• First, load the axiom set into the shared memory database like this:

./gkc -readkb NLP001+0.ax

• Second, ask a question using this pre-loaded data and a specified strategy like this:

./gkc -provekb kyss.txt query.txt 

where kyss.txt is a question file, two examples where "kyss" is the name of the formula

and the "conjecture" means that we want to prove whether

axioms => question

is true,

i.e. we do not negate the question (use "negated_conjecture" if the question is already negated):

fof(kyss,conjecture,(
    meronym__part(n2958343,n2670683) )).

and

% Cytogeneticist is a hyponym of biologist?

fof(axiom1,assumption,(
    ! [X,Y,Z] :
      ( ( hypernym(X,Y)
        & hypernym(Y,Z) )
     => hypernym(X,Z) ) )).

fof(axiom2,assumption,(
    ! [X,Y] :
      ( hypernym(X,Y)
     => hyponym(Y,X) ) )).

fof(axiom3,assumption,(
    ! [X,Y] :
      ( hyponym(X,Y)
     => hypernym(Y,X) ) )).

fof(hypernym_transitiviy_1,conjecture,(
    hypernym(n9986904,n9855630) )).

and

% there exists a kind of a wheeled vehicle with accelerator as a part

fof(axiom1,assumption,(
    ! [X,Y,Z] :
      ( ( hypernym(X,Y)
        & hypernym(Y,Z) )
     => hypernym(X,Z) ) )).

fof(axiom2,assumption,(
    ! [X,Y] :
      ( hypernym(X,Y)
     => hyponym(Y,X) ) )).

fof(axiom3,assumption,(
    ! [X,Y] :
      ( hyponym(X,Y)
     => hypernym(Y,X) ) )).

fof(kyss,conjecture,(
   lexicalization(M,'wheeled vehicle') &
   lexicalization(A,accelerator) &
   hypernym(X,M) & meronym__part(X,A) )).

and query.txt is the strategy selection file, use:

{
"max_size": 0,
"max_depth": 0,
"max_length":0,
"max_seconds": 0,
"strategy":["query_focus"],
"query_preference": 2
}