Riis, Søren; Sitharam, Meera Generating hard tautologies using predicate logic and the symmetric group. (English) Zbl 0967.03012 Log. J. IGPL 8, No. 6, 787-795 (2000). Methods to generate uniform families of hard propositional tautologies are presented. The tautologies are essentially generated from a single propositional formula by a natural action of the symmetric permutation group. The basic idea is that any second-order existential sentence can be systematically translated into a finite collection of clauses such that the models of an appropriate skolemization are in one-to-one correspondence with the satisfying assignments to the clauses. Under the assumption NEXPTIME\(\neq\)co-NEXPTIME, for any such sequence for which the spectrum is NEXPTIME-complete, certain tautologies do not have polynomial length proofs in any propositional proof system.The translation method shows that most sequences of tautologies being studied in propositional proof complexity can be systematically generated from second-order existential sentences and, moreover, many natural mathematical statements can be converted into sequences of propositional tautologies in this manner. Reviewer: U.Schöning (Ulm) Cited in 3 Documents MSC: 03B35 Mechanization of proofs and logical operations 03F20 Complexity of proofs 68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) 03C13 Model theory of finite structures Keywords:satisfiability; finite model theory; complexity theory; hard propositional tautologies; symmetric permutation group; propositional proof system; propositional proof complexity; second-order existential sentences PDFBibTeX XMLCite \textit{S. Riis} and \textit{M. Sitharam}, Log. J. IGPL 8, No. 6, 787--795 (2000; Zbl 0967.03012) Full Text: DOI Link