Search research articles

ABOUT JoVE

Overview Leadership Blog JoVE Help Center

AUTHORS

Publishing Process Editorial Board Scope & Policies Peer Review FAQ Submit

LIBRARIANS

Testimonials Subscriptions Access Resources Library Advisory Board FAQ

RESEARCH

JoVE Journal Methods Collections JoVE Encyclopedia of Experiments Archive

EDUCATION

JoVE Core JoVE Business JoVE Science Education JoVE Lab Manual Faculty Resource Center Faculty Site

Terms & Conditions of Use

Related Concept Videos

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by

Same author

LogiKEy workbench: Deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle/HOL dataset).

Data in brief·2020

Same author

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.

Journal of automated reasoning·2020

Same author

Universal (meta-)logical reasoning: The Wise Men Puzzle (Isabelle/HOL dataset).

Data in brief·2019

Same author

Computational logic: its origins and applications.

Proceedings. Mathematical, physical, and engineering sciences·2018

Search research articles

Related Experiment Video

Updated: Feb 5, 2026

Author Spotlight: Enhancing Microinjection Needle Quality by Wet Beveling

Author Spotlight: Enhancing Microinjection Needle Quality by Wet Beveling

Published on: September 27, 2024

The Higher-Order Prover Leo-II.

Christoph Benzmüller¹, Nik Sultana², Lawrence C Paulson²

¹Department of Mathematics and Computer Science, Freie Universität Berlin, Berlin, Germany.

Journal of Automated Reasoning

|September 4, 2018

Summary

Leo-II, an automated theorem prover for higher-order logic, enhances proof automation and standardization. Recent work focuses on its integration with proof assistants like Isabelle/HOL for verified proofs.

Keywords:

Automated theorem proving Higher-order logic Proof assistant

More Related Videos

Identification of Fatty Acids in Bacillus cereus

Identification of Fatty Acids in Bacillus cereus

Published on: December 5, 2016

Culturing of Human Nasal Epithelial Cells at the Air Liquid Interface

Culturing of Human Nasal Epithelial Cells at the Air Liquid Interface

Published on: October 8, 2013

Related Experiment Videos

Last Updated: Feb 5, 2026

Author Spotlight: Enhancing Microinjection Needle Quality by Wet Beveling

Author Spotlight: Enhancing Microinjection Needle Quality by Wet Beveling

Published on: September 27, 2024

Identification of Fatty Acids in Bacillus cereus

Identification of Fatty Acids in Bacillus cereus

Published on: December 5, 2016

Culturing of Human Nasal Epithelial Cells at the Air Liquid Interface

Culturing of Human Nasal Epithelial Cells at the Air Liquid Interface

Published on: October 8, 2013

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.