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

Abstract We introduce , an automated reasoning tool that analyses matrices generated by Slaney’s . 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 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 which do not witness variable sharing, and close with an appendix explaining how to install and use .