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

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

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.