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

Kohlhase M, Rabe F, Sacerdoti Coen C, Schaefer JF (2020)

Publication Type: Conference contribution

Publication year: 2020

Journal

Lecture Notes in Computer Science Springer Verlag

Publisher: Springer

Book Volume: 12166 LNAI

Pages Range: 395-401

Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Event location: Virtual, Online

ISBN: 9783030510732

DOI: 10.1007/978-3-030-51074-9_22

Abstract

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 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.

Authors with CRIS profile

Michael Kohlhase Professur für Wissensrepräsentation und -verarbeitung Florian Rabe Professur für Wissensrepräsentation und -verarbeitung Jan Frederik Schaefer Professur für Wissensrepräsentation und -verarbeitung

Involved external institutions

University of Bologna / Università di Bologna IT Italy (IT)

How to cite

APA:

Kohlhase, M., Rabe, F., Sacerdoti Coen, C., & Schaefer, J.F. (2020). Logic-Independent Proof Search in Logical Frameworks: (Short Paper). In Nicolas Peltier, Viorica Sofronie-Stokkermans (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 395-401). Virtual, Online: Springer.

MLA:

Kohlhase, Michael, et al. "Logic-Independent Proof Search in Logical Frameworks: (Short Paper)." Proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, Virtual, Online Ed. Nicolas Peltier, Viorica Sofronie-Stokkermans, Springer, 2020. 395-401.

BibTeX: Download