{'fraction_non_alphanumeric': 0.026436781609195402, 'fraction_numerical': 0.0011494252873563218, 'mean_word_length': 4.6558441558441555, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Feasible Proofs of Szpilrajn's Theorem - A Proof-Complexity Framework for Concurrent Automata

The aim of this paper is to propose a proof-complexity framework for concurrent automata. Since the behavior of concurrent processes can be described with partial orders, we start by formalizing proofs of Szpilrajn’s theorem. This theorem says that any partial order may be extended to a total order. We give two feasible proofs of the finite case of Szpilrajn’s theorem. The first proof is formalized in the logical theory LA extended to ordered rings; this yields a TC Frege derivation. The second proof is formalized in the logical theory ∃LA and yields a P/poly Frege derivation. Although TC is a much smaller complexity class than P/poly, the trade-off is that the P/poly proof is algebraically simpler—it requires the algebraic theory LA over the simplest of rings: Z2.