CNF generation software and article
Sam Buss
FmlaImplyChain and FmlaEquivChain CNFs
generation (C++ software)
Sam Buss
"FmlaChain: Formula Equivalence Chains
and Implication Chains as Tautologies",
preprint, October 2023.
Download preprint version of a paper describing the FmlaChain CNF's and software.
Based on the CNFs described in the paper Short Refutations for the Equivalence Chain Principle for Constant-Depth Formulas (S. Buss and Ramyaa, Mathematical Logic Quarterly, 2018).
Download FmlaChain.cpp, a C++ program for generating FmlaEquivChain and FmlaImplyChain CNFs.
Download FmlaChain_CNFs.zip, with several pre-generated instances of FmlaEquivChain and FmlaImplyChain CNF's.