Scholarlink

<p>We revisit a longstanding question about the shortest single axioms for positive implicational logic. Meredith discovered several 17-symbol single axioms and asked whether shorter ones exist. Later work reduced the problem to four candidate formulas of length 15. Using the automated theorem prover Vampire, we compute saturated clause sets that yield counter models showing that three of these candidates are not single axioms. This demonstrates the effectiveness of saturation-based reasoning for such problems, which have traditionally been studied via finite model searches.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Applying Saturation-Based Theorem Proving to Open Problems in Positive Implicational Logic

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年3月18日

查看全文
  • Branden Fitelson,
  • Nicolas Peltier

摘要

We revisit a longstanding question about the shortest single axioms for positive implicational logic. Meredith discovered several 17-symbol single axioms and asked whether shorter ones exist. Later work reduced the problem to four candidate formulas of length 15. Using the automated theorem prover Vampire, we compute saturated clause sets that yield counter models showing that three of these candidates are not single axioms. This demonstrates the effectiveness of saturation-based reasoning for such problems, which have traditionally been studied via finite model searches.