The Higher-Order Prover Leo-II

Area of Science:

• Automated reasoning
• Higher-order logic
• Formal verification

Background:

• Leo-II is a key automated theorem prover for classical higher-order logic.
• It has significantly influenced the development of the TPTP THF infrastructure.
• Leo-II has a history of successful application across diverse problem domains.

Purpose of the Study:

• To report on recent advancements in integrating Leo-II with proof assistants.
• To ensure Leo-II's proof output is in a standardized syntax for verification.
• To enhance user effort reduction within proof assistants through external theorem proving.

Main Methods:

• Development of standardized proof output formats for Leo-II.
• Integration of Leo-II as an external tool within proof assistant frameworks.
• Focus on compatibility with systems like Isabelle/HOL for proof transformation.

Main Results:

• Progress has been made in enabling Leo-II to return standardized proof information.
• This facilitates the transformation and verification of proofs within proof assistants.
• The integration aims to streamline the process of formal verification.

Conclusions:

• Standardized proof output from Leo-II is crucial for its utility in proof assistants.
• Recent developments show promise for seamless integration and verification.
• Leo-II continues to be a valuable tool in advancing automated theorem proving and formal methods.