The Higher-Order Prover Leo-II

Leo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order–first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic, and it has been applied in a wide array of problems. Leo-II...

Descripción completa

Detalles Bibliográficos
Autores principales: Benzmüller, Christoph, Sultana, Nik, Paulson, Lawrence C., Theiß, Frank
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Netherlands 2015
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6109767/
https://www.ncbi.nlm.nih.gov/pubmed/30174358
http://dx.doi.org/10.1007/s10817-015-9348-y
_version_ 1783350375015776256
author Benzmüller, Christoph
Sultana, Nik
Paulson, Lawrence C.
Theiß, Frank
author_facet Benzmüller, Christoph
Sultana, Nik
Paulson, Lawrence C.
Theiß, Frank
author_sort Benzmüller, Christoph
collection PubMed
description Leo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order–first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic, and it has been applied in a wide array of problems. Leo-II may also be called in proof assistants as an external aid tool to save user effort. For this it is crucial that Leo-II returns proof information in a standardised syntax, so that these proofs can eventually be transformed and verified within proof assistants. Recent progress in this direction is reported for the Isabelle/HOL system.
format Online
Article
Text
id pubmed-6109767
institution National Center for Biotechnology Information
language English
publishDate 2015
publisher Springer Netherlands
record_format MEDLINE/PubMed
spelling pubmed-61097672018-08-31 The Higher-Order Prover Leo-II Benzmüller, Christoph Sultana, Nik Paulson, Lawrence C. Theiß, Frank J Autom Reason Article Leo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order–first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic, and it has been applied in a wide array of problems. Leo-II may also be called in proof assistants as an external aid tool to save user effort. For this it is crucial that Leo-II returns proof information in a standardised syntax, so that these proofs can eventually be transformed and verified within proof assistants. Recent progress in this direction is reported for the Isabelle/HOL system. Springer Netherlands 2015-09-22 2015 /pmc/articles/PMC6109767/ /pubmed/30174358 http://dx.doi.org/10.1007/s10817-015-9348-y Text en © The Author(s) 2015 Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
spellingShingle Article
Benzmüller, Christoph
Sultana, Nik
Paulson, Lawrence C.
Theiß, Frank
The Higher-Order Prover Leo-II
title The Higher-Order Prover Leo-II
title_full The Higher-Order Prover Leo-II
title_fullStr The Higher-Order Prover Leo-II
title_full_unstemmed The Higher-Order Prover Leo-II
title_short The Higher-Order Prover Leo-II
title_sort higher-order prover leo-ii
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6109767/
https://www.ncbi.nlm.nih.gov/pubmed/30174358
http://dx.doi.org/10.1007/s10817-015-9348-y
work_keys_str_mv AT benzmullerchristoph thehigherorderproverleoii
AT sultananik thehigherorderproverleoii
AT paulsonlawrencec thehigherorderproverleoii
AT theißfrank thehigherorderproverleoii
AT benzmullerchristoph higherorderproverleoii
AT sultananik higherorderproverleoii
AT paulsonlawrencec higherorderproverleoii
AT theißfrank higherorderproverleoii

Ejemplares similares