×

Generating hard tautologies using predicate logic and the symmetric group. (English) Zbl 0967.03012

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)

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
PDFBibTeX XMLCite
Full Text: DOI Link