Leo-III 1.7.15

Leo-III version 1.7.15.

Minor updates:

• Fixes relating to correct SZS status reporting
• Updated versions of scala library and other dependencies
• Updated embedding runtime for NCL reasoning
• Support for the TPTP $distinct predicate (experimental)

This version is used in CASC-J12 (http://tptp.org/CASC/J12/).

Leo-III 1.7

Leo-III version 1.7.

Minor updates:

• Fixes around ground arithmetic support
• Updated versions of scala library and other dependencies
• Updated embedding runtime for NCL reasoning

This version was used in CASC-J11 (http://tptp.org/CASC/J11/).

Leo-III 1.6

Leo-III version 1.6.

Minor updates:

• Small fixes in proof output when injective functions are present
• Added preliminary support for ground arithmetic
• Bump to Scala language version 2.13.5

This version was used in CASC-28 (http://tptp.org/CASC/28/).

Leo-III 1.5.2

Version 1.5.2 of Leo-III.
New features:

• Improved TH1 proof output
• Faster and more robust parser for TPTP inputs

Leo-III 1.5

Leo-III version 1.5 fixes some bugs of earlier versions. Used in CASC of 2020.

Leo-III 1.4

Leo-III version 1.4 fixes some bugs of earlier versions and a slightly updated documentation.

Leo-III 1.3

Pre-release of Leo-III 1.3.

New features: TBA

Leo-III 1.2

Version 1.2 of Leo-III features several improvements and new features, including:

• Improved reasoning capabilities for polymorphic input problems (TF1, TH1)
• Native support for higher-order modal logic (see README for details)
• Special reasoning capabilities for problems containing injective functions
• Function synthesis routines (--funcspec)
• Several bug fixes and improved general performance

Leo-III 1.1b

Version 1.1 of the automated theorem prover Leo-III for classical higher-order logic with choice.
This version corresponds to the version submitted to CASC-26 with
slight modifications in the build process.

For details, we refer to the system description presented at IWIL-2017 or visit our project website.

Leo-III 1.1

Version 1.1 of the automated theorem prover Leo-III for classical higher-order logic with choice.
This version corresponds to the version submitted to CASC-26.

For details, we refer to the system description presented at IWIL-2017 or visit our project website.