Scholarlink

<p>We introduce <Emphasis FontCategory="NonProportional">VSPursuer</Emphasis>, an automated reasoning tool that analyses matrices generated by Slaney’s <Emphasis FontCategory="NonProportional">MaGIC</Emphasis>. The tool searches these matrices for a target logic to find one that witnesses the logic’s satisfaction of the <i>Variable Sharing Property</i>. We describe the theoretical background behind <Emphasis FontCategory="NonProportional">VSPursuer</Emphasis> and highlight optimisations that enable our tool to determine whether a given matrix witnesses the property in polynomial time. We then give some example data sets for particular relevant logics, a theoretical analysis on the sizes of matrices generated by <Emphasis FontCategory="NonProportional">MaGIC</Emphasis> which do not witness variable sharing, and close with an appendix explaining how to install and use <Emphasis FontCategory="NonProportional">VSPursuer</Emphasis>.</p>

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

VSPursuer: A Tool for Finding Matrices Witnessing the Variable Sharing Property

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年2月9日

查看全文
  • Brandon Rozek,
  • Andrew Tedder

摘要

We introduce VSPursuer, an automated reasoning tool that analyses matrices generated by Slaney’s MaGIC. The tool searches these matrices for a target logic to find one that witnesses the logic’s satisfaction of the Variable Sharing Property. We describe the theoretical background behind VSPursuer and highlight optimisations that enable our tool to determine whether a given matrix witnesses the property in polynomial time. We then give some example data sets for particular relevant logics, a theoretical analysis on the sizes of matrices generated by MaGIC which do not witness variable sharing, and close with an appendix explaining how to install and use VSPursuer.