Shortening of Proof Length is Elusive for Theorem Provers

DOI10.1142/S0129626420500139zbMath1490.68291OpenAlexW3120358209MaRDI QIDQ5087078

Wilfried Sieg, Francisco Hernández-Quiroz, Hector Zenil, Santiago Hernández-Orozco

Publication date: 8 July 2022

Published in: Parallel Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1142/s0129626420500139

zbMATH Keywords

computational complexityalgorithmic complexitypropositional calculusautomatic theorem provingexperimental mathematicstrade-offs of complexity measures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isabelle
• Isabelle/Isar
• Isar
• Prover9
• Mace4

Cites Work

• Normal natural deduction proofs (in classical logic)
• Minimum propositional proof length is NP-hard to linearly approximate
• Computer Runtimes and the Length of Proofs
• The AProS Project: Strategic Thinking & Computational Logic

This page was built for publication: Shortening of Proof Length is Elusive for Theorem Provers