Certified Connection Tableaux Proofs for HOL Light and TPTP

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F15%3A00225199" target="_blank" >RIV/68407700:21230/15:00225199 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Certified Connection Tableaux Proofs for HOL Light and TPTP

Popis výsledku v původním jazyce

In recent years, the Metis prover based on ordered paramodulation and model elimination has replaced the earlier built-in methods for general-purpose proof automation in HOL4 and Isabelle/HOL. In the annual CASC competition, the leanCoP system based on connection tableaux has however performed better than Metis. In this paper we show how the leanCoP?s core algorithm can be implemented inside HOL Light. leanCoP?s flagship feature, namely its minimalistic core, results in a very simple proof system. Thisplays a crucial role in extending the MESON proof reconstruction mechanism to connection tableaux proofs, providing an implementation of leanCoP that certifies its proofs. We discuss the differences between our direct implementation using an explicit Prolog stack, to the continuation passing implementation of MESON present in HOL Light and compare their performance on all core HOL Light goals. The resulting prover can be also used as a general purpose TPTP prover. We compare its performa

Název v anglickém jazyce

Certified Connection Tableaux Proofs for HOL Light and TPTP

Popis výsledku anglicky

In recent years, the Metis prover based on ordered paramodulation and model elimination has replaced the earlier built-in methods for general-purpose proof automation in HOL4 and Isabelle/HOL. In the annual CASC competition, the leanCoP system based on connection tableaux has however performed better than Metis. In this paper we show how the leanCoP?s core algorithm can be implemented inside HOL Light. leanCoP?s flagship feature, namely its minimalistic core, results in a very simple proof system. Thisplays a crucial role in extending the MESON proof reconstruction mechanism to connection tableaux proofs, providing an implementation of leanCoP that certifies its proofs. We discuss the differences between our direct implementation using an explicit Prolog stack, to the continuation passing implementation of MESON present in HOL Light and compare their performance on all core HOL Light goals. The resulting prover can be also used as a general purpose TPTP prover. We compare its performa

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP103%2F12%2F1994" target="_blank" >GAP103/12/1994: Adaptivní algoritmy pro rozvrhování a optimalizaci distribuovaných vestavěných real-time systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 2015 Conference on Certified Programs and Proofs

ISBN

978-1-4503-3296-5

ISSN

—

e-ISSN

—

Počet stran výsledku

8

Strana od-do

59-66

Název nakladatele

ACM

Místo vydání

New York

Místo konání akce

Mumbai

Datum konání akce

13. 1. 2015

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—