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.
Logic-Independent Proof Search in Logical Frameworks: (Short Paper) / Kohlhase M.; Rabe F.; Sacerdoti Coen C.; Schaefer J.F.. - STAMPA. - 12166:(2020), pp. 395-401. (Intervento presentato al convegno 10th International Joint Conference on Automated Reasoning, IJCAR 2020 tenutosi a Paris nel 01-04/07/2020) [10.1007/978-3-030-51074-9_22].
Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
Sacerdoti Coen C.;
2020
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.