Logic-independent proof search in logical frameworks (short paper)

DOI10.1007/978-3-030-51074-9_22OpenAlexW3039099885MaRDI QIDQ2096460

Jan Frederik Schaefer, Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_22

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Isabelle
• LEO-II
• MetTeL
• GF
• LATIN
• GitHub

Cites Work

• Isabelle. A generic theorem prover
• How to identify, translate and combine logics?
• ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• A framework for defining logics
• Resource-Adaptive Model Generation as a Performance Model
• A Modular Type Reconstruction Algorithm
• Grammatical Framework
• Foundational Proof Certificates in First-Order Logic
• Project Abstract: Logic Atlas and Integrator (LATIN)

This page was built for publication: Logic-independent proof search in logical frameworks (short paper)