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

DOI10.1007/978-3-030-51074-9_22MaRDI QIDQ2096460zbMATH OpenOpenAlexFDO

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

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)

Cites work

• A framework for defining logics
• A Modular Type Reconstruction Algorithm
• ELPI: fast, embeddable, Prolog interpreter
• Foundational proof certificates in first-order logic
• Grammatical Framework
• How to identify, translate and combine logics?
• Isabelle. A generic theorem prover
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Project abstract: logic atlas and integrator (LATIN)
• Resource-Adaptive Model Generation as a Performance Model

Cited in

(1)

• Efficient SAT-based proof search in intuitionistic propositional logic

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2096460)