Logic-Independent Proof Search in Logical Frameworks: (Short Paper)

Logical frameworks like LF allow to specify the syntax and (natural deduction) inference rules for syntax/proof-checking a wide variety of logical systems. A crucial feature that is missing for prototyping logics is a way to specify basic proof automation. We try to alleviate this problem by generat...

Descripción completa

Detalles Bibliográficos
Autores principales: Kohlhase, Michael, Rabe, Florian, Sacerdoti Coen, Claudio, Schaefer, Jan Frederik
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324214/
http://dx.doi.org/10.1007/978-3-030-51074-9_22
_version_ 1783551893992112128
author Kohlhase, Michael
Rabe, Florian
Sacerdoti Coen, Claudio
Schaefer, Jan Frederik
author_facet Kohlhase, Michael
Rabe, Florian
Sacerdoti Coen, Claudio
Schaefer, Jan Frederik
author_sort Kohlhase, Michael
collection PubMed
description Logical frameworks like LF allow to specify the syntax and (natural deduction) inference rules for syntax/proof-checking a wide variety of logical systems. A crucial feature that is missing for prototyping logics is a way to specify basic proof automation. We try to alleviate this problem by generating [Formula: see text]Prolog (ELPI) inference predicates from logic specifications and controlling them by logic-independent helper predicates that encapsulate the prover characteristics. We show the feasibility of the approach with three experiments: We directly automate ND calculi, we generate tableau theorem provers and model generators.
format Online
Article
Text
id pubmed-7324214
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73242142020-06-30 Logic-Independent Proof Search in Logical Frameworks: (Short Paper) Kohlhase, Michael Rabe, Florian Sacerdoti Coen, Claudio Schaefer, Jan Frederik Automated Reasoning Article Logical frameworks like LF allow to specify the syntax and (natural deduction) inference rules for syntax/proof-checking a wide variety of logical systems. A crucial feature that is missing for prototyping logics is a way to specify basic proof automation. We try to alleviate this problem by generating [Formula: see text]Prolog (ELPI) inference predicates from logic specifications and controlling them by logic-independent helper predicates that encapsulate the prover characteristics. We show the feasibility of the approach with three experiments: We directly automate ND calculi, we generate tableau theorem provers and model generators. 2020-05-30 /pmc/articles/PMC7324214/ http://dx.doi.org/10.1007/978-3-030-51074-9_22 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Kohlhase, Michael
Rabe, Florian
Sacerdoti Coen, Claudio
Schaefer, Jan Frederik
Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
title Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
title_full Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
title_fullStr Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
title_full_unstemmed Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
title_short Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
title_sort logic-independent proof search in logical frameworks: (short paper)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324214/
http://dx.doi.org/10.1007/978-3-030-51074-9_22
work_keys_str_mv AT kohlhasemichael logicindependentproofsearchinlogicalframeworksshortpaper
AT rabeflorian logicindependentproofsearchinlogicalframeworksshortpaper
AT sacerdoticoenclaudio logicindependentproofsearchinlogicalframeworksshortpaper
AT schaeferjanfrederik logicindependentproofsearchinlogicalframeworksshortpaper

Ejemplares similares