Certified Connection Tableaux Proofs for HOL Light and TPTP
The result's identifiers
Result code in 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>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Certified Connection Tableaux Proofs for HOL Light and TPTP
Original language description
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
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GAP103%2F12%2F1994" target="_blank" >GAP103/12/1994: Adaptive scheduling and Optimization algorithms for distributed Real-time Embeddes Systems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2015
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the 2015 Conference on Certified Programs and Proofs
ISBN
978-1-4503-3296-5
ISSN
—
e-ISSN
—
Number of pages
8
Pages from-to
59-66
Publisher name
ACM
Place of publication
New York
Event location
Mumbai
Event date
Jan 13, 2015
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—