Towards structurally-free theorem proving

DOI10.1093/JIGPAL/6.3.425MaRDI QIDQ4392659zbMATH OpenOpenAlexFDO

Authors Marcelo Finger

Publication date 22 February 1999

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/ec7a0289126586ee705840d9fdd44dc7cb19268e

zbMATH Keywords

algorithmcombinator rulesdecision procedureequistructural transformationsGentzen systemslambda calculusstructurally free logicstheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Review text

The aim of the paper is to provide a formal basis for computing in which logics a given formula is elucidable. This task is accomplished in the context of structurally free logics. In these logics the usual structural rules are replaced by complex combinator rules. In this setting, structurally free theorem proving is a decision procedure that inputs a formula and outputs the corresponding combinator when the formula is deducible. An algorithm is presented to compute a combinator corresponding to a given formula (if it exists). The algorithm is based on equistructural transformations. It is shown that this algorithm is sound and complete and always terminates.

Recommendations

• Theorem provers for substructural logics
• Free deduction: An analysis of ``computations in classical logic
• A family of goal directed theorem provers based on conjunction and implication. I
• Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories

Cited in

(1)

• Theorem provers for substructural logics

This page was built for publication: Towards structurally-free theorem proving

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