Experimental analysis reveals bimodal distribution of proof complexity in Boolean rings, suggesting insights into LRPO effects.
In this paper, we present an experiment of complex effects of LRPO on the proof complexity in term orderings on algebraic structures. In experiment, we yield 10! lex patterns that are derived from the symbols that make up Boolean rings (+, −,×, #,∧, 0, 1, a, b, c). Also, the given clause algorithm is used to measure the proof complexity by counting the number of clauses generated. Curiously, the experimental results showed that the distribution the proof complexity was not unimodal, but bimodal. We discuss three possible reasons of bimodality of proof complexity in algebraic structures.
No takes yet. Share an insight, caveat, or question.
Ando et al. (2025) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: