Short proofs for tricky formulas

DOI10.1007/BF00265682zbMath0552.03009MaRDI QIDQ800909

Balakrishnan Krishnamurthy

Publication date: 1985

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

symmetry; Ramsey numbers; extension; resolution; formal proofs; propositional calculus; acyclic digraph; checkerboard puzzle; inductive arguments; propositional tautologies

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

Related Items

Exploiting Symmetry in SMT Problems, The limits of tractability in resolution-based propositional proof systems, Symmetric blocking, \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, 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, Regular and General Resolution: An Improved Separation, Local Symmetry Breaking During Search in CSPs, An Exponential Lower Bound for Width-Restricted Clause Learning