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)

Recommendations

• Theorem provers for substructural logics
• scientific article; zbMATH DE number 1337625
• 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)