Short proofs for tricky formulas
The object of this paper is to demonstrate how certain tricky mathematical arguments can be encoded as short formal proofs for the propositional tautologies representing the mathematical statements. Using resolution as a base proof system for the propositional calculus, we exhibit these short proofs under resolution augmented by one of two principles: the principle of extension, originally suggested by Tseitin, and the principle of symmetry, introduced in this paper. These short proofs illustrate the power of extension and symmetry in theorem proving. The principle of extension allows the introduction of auxiliary variables to represent intermediate formulas so that the length of a proof can be significantly reduced by manipulating these variables instead of the formulas that they stand for. Symmetry, on the other hand, allows one to recognize that a tautology remains invariant under certain permutations of variable names, and use that information to avoid repeated independent derivations of intermediate formulas that are merely permutational variants of one another. First we show that a number of inductive arguments can be encoded as short formal proofs using either extension or symmetry. We provide the details for the tautologies derived by encoding the statement, An acyclic digraph on n vertices must have a source. We then consider the familiar checkerboard puzzle which asserts that a checkerboard, two of whose diagonally opposite corner squares are removed, cannot be perfectly covered with dominoes. We demonstrate short proofs for the tautologies derived from the above assertion, using extension to mimic the tricky informal argument. Finally, we consider statements asserting the Ramsey property of numbers much larger than the critical Ramsey numbers. We show that the proof of Ramsey's theorem can be imitated using the principle of symmetry to yield short proofs for these tautologies. The main theme of the paper is that both extension and symmetry are very powerful augmentations to resolution. We leave open wether either extension or symmetry can polynomially simulate the other.
- \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
- Tractability through symmetries in propositional calculus
- Homomorphisms of conjunctive normal forms.
- Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
- On the decision trees with symmetries
- The complexity of resolution with generalized symmetry rules
- Testing satisfiability of CNF formulas by computing a stable set of points
- The complexity of homomorphisms and renamings for minimal unsatisfiable formulas
- Short proofs for some symmetric quantified Boolean formulas
- Mutilated chessboard problem is exponentially hard for resolution
- Short resolution proofs for a sequence of tricky formulas
- The symmetry rule in propositional logic
- Formula simplification via invariance detection by algebraically indexed types
- Propositional proof systems based on maximum satisfiability
- Symmetries, almost symmetries, and lazy clause generation
- Local and global symmetry breaking in itemset mining
- Separation results for the size of constant-depth propositional proofs
- The state of SAT
- How to find symmetries hidden in combinatorial problems
- Regular and General Resolution: An Improved Separation
- Local Symmetry Breaking During Search in CSPs
- An Exponential Lower Bound for Width-Restricted Clause Learning
- The limits of tractability in resolution-based propositional proof systems
- scientific article; zbMATH DE number 1324437 (Why is no real title available?)
- scientific article; zbMATH DE number 1348469 (Why is no real title available?)
- scientific article; zbMATH DE number 1555175 (Why is no real title available?)
- Ground resolution with group computations on semantic symmetries
- On linear resolution
- Resolution and the binary encoding of combinatorial principles
- Sum of squares bounds for the ordering principle
- Exploiting symmetry in SMT problems
- Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas
- Proof complexity and the binary encoding of combinatorial principles
- Resolution with symmetry rule applied to linear equations
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Symmetric blocking
This page was built for publication: Short proofs for tricky formulas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q800909)
