v0.8.0

The compiled Linux binary and a source snapshot of the gkc version 0.8.0 for the CASC 2023 competition http://www.tptp.org/CASC/29/

You may want to use the previous release 0.6.0 for non-competition purposes: it includes MacOS and Windows binaries, matches the tutorial and is a basis for http://logictools.org.

Binaries

• gkc is a statically compiled 64-bit executable Linux binary, created on Ubuntu Linux 20 using gcc 9.4. It should have no dependencies.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc problem_file_name strategy_file_name

Please see

• Examples/README.md in https://github.com/tammet/gkc for a detailed tutorial with examples.
• README.md https://github.com/tammet/gkc for a brief overview and compilation guides.

v0.7.0

The compiled Linux binary and a source snapshot of the gkc version 0.7.0 for the CASC 2021 competition http://www.tptp.org/CASC/28/

You may want to use the previous release 0.6.0 for non-competition purposes: it includes MacOS and Windows binaries, matches the tutorial and is a basis for http://logictools.org.

Binaries

• gkc is a statically compiled 64-bit executable Linux binary, created on Ubuntu Linux 20 using gcc 9.3. It should have no dependencies.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc problem_file_name strategy_file_name

For the CASC LTB division please give the batch file and the output folder as arguments. For the LTB division gkc calls itself for all the problems, using bash via the system call. Thus it is important that gkc can find its own path using the readlink system call and can limit time using the timeout command on bash.

Please see

• Examples/README.md in https://github.com/tammet/gkc for a detailed tutorial with examples.
• README.md https://github.com/tammet/gkc for a brief overview and compilation guides.

v0.6.0

Compiled binaries and a source snapshot of the gkc version 0.6.0 introducing the JSON syntax option.

Binaries

• gkc is a statically compiled 64-bit executable Linux binary, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
• gkc.exe is a 64-bit executable Windows binary, created on Windows 10 using the 2017 Visual Studio C
  community edition command-line tool cl.
• gkc32.exe is a 32-bit executable Windows binary, created on Windows 10 using the 2017 Visual Studio C community edition command-line tool cl.
• gkcosx is a an OS X (macOS) binary, created on macOS Catalina 10.15.4 with the Apple clang version 11.0.3.
• gkcjs.wasm and gkcjs.js are Wasm binaries created by emscripten for running in the browser: see logictools.org.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc problem_file_name strategy_file_name

Please see

• Examples/README.md in https://github.com/tammet/gkc for a detailed tutorial with examples.
• README.md https://github.com/tammet/gkc for a brief overview and compilation guides.

v0.5.2

Compiled binaries of the gkc version 0.5.2: fixing several issues found in the earlier version submitted to CASC 2020.

Binaries

• gkc is a statically compiled 64-bit executable Linux binary for the gkc version 0.5.2, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
• gkc.exe is a 64-bit executable Windows binary for the gkc version 0.5.2, created on Windows 10 using the 2017 Visual Studio C
  community edition command-line tool cl.
• gkc32.exe is a 32-bit executable Windows binary for the gkc version 0.5.2, created on Windows 10 using the 2017 Visual Studio C community edition command-line tool cl.
• gkcosx is a an OS X (macOS) binary for the gkc version 0.5.2, created on macOS Catalina 10.15.4 with the Apple clang version 11.0.3.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc problem_file_name strategy_file_name

Please see

• Examples/README.md in https://github.com/tammet/gkc for a detailed tutorial with examples.
• README.md https://github.com/tammet/gkc for a brief overview and compilation guides.

v0.5.1-casc

Compiled binaries of the gkc version 0.5.1 submitted to CASC 2020.

Binaries

• gkc is a statically compiled 64-bit executable binary for the gkc version 0.5.1, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
• For the windows binary look for newer or older releases.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc -prove problem_file_name strategy_file_name

Please see the README.md in https://github.com/tammet/gkc for additional details

v0.5.0-casc

Compiled binaries of the gkc version 0.5.0 submitted to CASC 2020.

Binaries

• gkc is a statically compiled 64-bit executable binary for the gkc version 0.5.0, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
• For the windows binary look for newer or older releases.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc -prove problem_file_name strategy_file_name

Please see the README.md in https://github.com/tammet/gkc for additional details.

v0.4.1-casc

Compiled binaries of the gkc version 0.4.1 as used in CASC 2019 for LTB, plus error handling improvements.

Compared to 4.0, the LTB-related shared db fix was applied.

Binaries

• gkc is a statically compiled 64-bit executable binary for the gkc version 0.4.1, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
• gkc.exe is a 32-bit Windows executable, compiled on Windows 10 using the Visual Studio community edition command line compiler.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc -prove problem_file_name strategy_file_name

Please see the README.md in https://github.com/tammet/gkc for additional details.

v0.4-casc

Compiled binaries of the gkc version 0.4 as used in CASC 2019.

Result output format, ltb division include and memory leakage fixes were applied.

Binaries

• gkc is a statically compiled 64-bit executable binary for the gkc version 0.4, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
• gkc.exe is a 32-bit Windows executable, compiled on Windows 10 using the Visual Studio community edition command line compiler.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc -prove problem_file_name strategy_file_name

Please see the README.md in https://github.com/tammet/gkc for additional details.

v0.1-epsilon

Compiled binaries of the gkc development version snapshot 0.1.

This release fixes a few errors in the previous release and introduces some efficiency improvements.

Binaries

• gkc is a statically compiled executable binary for the gkc version 0.1-epsilon, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
• gkc.zip is a zipped executable gkc.exe for Windows, compiled on Windows 10 using the Visual Studio community edition command line compiler.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc -prove problem_file_name strategy_file_name

example:

./gkc -prove /opt/TPTP/Problems/NUM/NUM925+5.p runs.txt

where

• -prove is a command to gkc
• problem_file_name is a problem file in TPTP syntax, possibly containing include commands like include('Axioms/CSR002+5.ax'). The included files are searched either from the local folder or a fixed
  path opt/TPTP/ . For this exam the file opt/TPTP/Axioms/CSR002+5.ax would be looked up.
  The TPTP problems and axioms are not included in the gkc distribution:
  for the TPTP syntax and problems, see http://www.tptp.org/
• strategy_file_name is a json-syntax file for giving options and strategies to gkc. See and use the
  example files unit.txt, neg.txt, strat.txt in the Examples folder.

For all options of running gkc, including the shared memory database usage, see

./gkc -help

Experimental results

Please see the full logs for the CASC-j9 FOF division problems in an earlier release
https://github.com/tammet/gkc/releases/tag/v0.1-alpha

v0.1-delta

Compiled binaries of the gkc development version snapshot 0.1.

This releases fixes several errors in the previous release, which enabled shared memory database usage via the -readkb, -provekb, -deletekb command line arguments. Run ./gkc -help for instructions.

Binaries

• gkc is a statically compiled executable binary for the gkc version 0.1-delta, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
• gkc.zip is a zipped executable gkc.exe for Windows, compiled on Windows 10 using the Visual Studio community edition command line compiler.

Running gkc

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc -prove problem_file_name strategy_file_name

example:

./gkc -prove /opt/TPTP/Problems/NUM/NUM925+5.p runs.txt

where

• -prove is a command to gkc
• problem_file_name is a problem file in TPTP syntax, possibly containing include commands like include('Axioms/CSR002+5.ax'). The included files are searched either from the local folder or a fixed
  path opt/TPTP/ . For this exam the file opt/TPTP/Axioms/CSR002+5.ax would be looked up.
  The TPTP problems and axioms are not included in the gkc distribution:
  for the TPTP syntax and problems, see http://www.tptp.org/
• strategy_file_name is a json-syntax file for giving options and strategies to gkc. See and use the
  example files unit.txt, neg.txt, strat.txt in the Examples folder.

For all options of running gkc, including the shared memory database usage, see

./gkc -help

Experimental results

Please see the full logs for the CASC-j9 FOF division problems in an earlier release
https://github.com/tammet/gkc/releases/tag/v0.1-alpha