Applying saturation-based theorem proving to open problems in positive implicational logic

DOI10.1007/S10817-026-09752-1MaRDI QIDQ6834471zbMATH OpenFDO

Authors Branden Fitelson, Nicolas Peltier

Publication date 31 March 2026

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-026-09752-1

zbMATH Keywords

automated theorem provingintuitionistic implicationpropositional logicsaturationsingle axioms

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A legacy recalled and a tradition continued
• scientific article; zbMATH DE number 1471997 (Why is no real title available?)
• scientific article; zbMATH DE number 3085173 (Why is no real title available?)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Notes on the axiomatics of the propositional calculus
• Stepping stones in the TPTP world

This page was built for publication: Applying saturation-based theorem proving to open problems in positive implicational logic

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