Short proofs for tricky formulas

DOI10.1007/BF00265682MaRDI QIDQ800909zbMATH OpenOpenAlexFDO

Authors Balakrishnan Krishnamurthy

Publication date 1985

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00265682

zbMATH Keywords

symmetryextensionresolutionRamsey numbersacyclic digraphformal proofspropositional calculuscheckerboard puzzleinductive argumentspropositional tautologies

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Tractability through symmetries in propositional calculus
• scientific article; zbMATH DE number 1348469
• The symmetry rule in propositional logic
• scientific article; zbMATH DE number 516991
• Short proofs are narrow—resolution made simple

Cited in

(34)

• On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
• Formula simplification via invariance detection by algebraically indexed types
• Resolution and the binary encoding of combinatorial principles
• Sum of squares bounds for the ordering principle
• The limits of tractability in resolution-based propositional proof systems
• The state of SAT
• Homomorphisms of conjunctive normal forms.
• Proof complexity and the binary encoding of combinatorial principles
• Tractability through symmetries in propositional calculus
• How to find symmetries hidden in combinatorial problems
• The complexity of homomorphisms and renamings for minimal unsatisfiable formulas
• Symmetries, almost symmetries, and lazy clause generation
• The symmetry rule in propositional logic
• On the decision trees with symmetries
• Propositional proof systems based on maximum satisfiability
• Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
• On linear resolution
• Regular and General Resolution: An Improved Separation
• Ground resolution with group computations on semantic symmetries
• The complexity of resolution with generalized symmetry rules
• Testing satisfiability of CNF formulas by computing a stable set of points
• Resolution with symmetry rule applied to linear equations
• Short resolution proofs for a sequence of tricky formulas
• Symmetric blocking
• Mutilated chessboard problem is exponentially hard for resolution
• Separation results for the size of constant-depth propositional proofs
• scientific article; zbMATH DE number 1555175 (Why is no real title available?)
• Short proofs for some symmetric quantified Boolean formulas
• Local and global symmetry breaking in itemset mining
• \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
• An Exponential Lower Bound for Width-Restricted Clause Learning
• Exploiting symmetry in SMT problems
• Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas
• Local Symmetry Breaking During Search in CSPs

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)