Short proofs for tricky formulas
From MaRDI portal
Publication:800909
DOI10.1007/BF00265682zbMath0552.03009MaRDI QIDQ800909
Publication date: 1985
Published in: Acta Informatica (Search for Journal in Brave)
symmetry; Ramsey numbers; extension; resolution; formal proofs; propositional calculus; acyclic digraph; checkerboard puzzle; inductive arguments; propositional tautologies
03B35: Mechanization of proofs and logical operations
Related Items
Exploiting Symmetry in SMT Problems, The limits of tractability in resolution-based propositional proof systems, \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, Testing satisfiability of CNF formulas by computing a stable set of points, The complexity of homomorphisms and renamings for minimal unsatisfiable formulas, Mutilated chessboard problem is exponentially hard for resolution, Short resolution proofs for a sequence of tricky formulas, The symmetry rule in propositional logic, Separation results for the size of constant-depth propositional proofs, The state of SAT, Regular and General Resolution: An Improved Separation, Local Symmetry Breaking During Search in CSPs, An Exponential Lower Bound for Width-Restricted Clause Learning
