Short resolution proofs for a sequence of tricky formulas

No abstract is available for this paper.

• Publication year

  1996

• Venue

  Acta Informatica

• Publication date

  1996-05-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/s002360050044
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Quasipolynomial size proofs of the propositional pigeonhole principle

  2015cited by this paper
• Algorithmic aspects of intuitionistic propositional logic II

  1987cited by this paper
• Short proofs for tricky formulas

  1985cited by this paper
• The Intractability of Resolution

  1985cited by this paper
• The Relative Efficiency of Propositional Proof Systems

  1979cited by this paper
• A short proof of the pigeon hole principle using extended resolution

  1976cited by this paper
• Gisbert Hasenjaeger. Über eine Art von Unvollständigkeit des Prädikatenkalküls der ersten Stufe. The journal of symbolic logic , vol. 15 (1950), 273–276.

  1951cited by this paper
• Über eine Art von Unvollständigkeit des Prädikatenkalküls der ersten Stufe

  1950cited by this paper
• Grundlagen der Mathematik

  1934cited by this paper

• Polynomial Calculus Sizes Over the Boolean and Fourier Bases are Incomparable

  2024cites this paper
• Proof Complexity and the Binary Encoding of Combinatorial Principles

  2024cites this paper
• Bounds on the Total Coefficient Size of Nullstellensatz Proofs of the Pigeonhole Principle and the Ordering Principle

  2022cites this paper
• Proof Complexity and SAT Solving

  2021cites this paper
• Large Clique is Hard on Average for Resolution

  2021cites this paper
• The power of negative reasoning

  2021cites this paper
• Typical forcings, NP search problems and an extension of a theorem of Riis

  2020cites this paper
• Proof complexity and the binary encoding of combinatorial principles

  2020cites this paper
• Typical forcings, NP search problems and an extension of a theorem of Riis

  2020influential citation
• Resolution and the binary encoding of combinatorial principles

  2018cites this paper
• Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

  2018cites this paper
• Space in Weak Propositional Proof Systems

  2018cites this paper
• Sum of squares bounds for the ordering principle

  2018cites this paper
• Sum of squares bounds for the total ordering principle

  2018cites this paper
• Some Subsystems of Constant-Depth Frege with Parity

  2018cites this paper
• A note about k-DNF resolution

  2018cites this paper
• The Treewidth of Proofs MoritzMüller and

  2017cites this paper
• CNFgen: A Generator of Crafted Benchmarks

  2017cites this paper
• On the Quest for an Acyclic Graph

  2017influential citation
• The treewidth of proofs

  2017cites this paper
• On Linear Resolution

  2016cites this paper
• On Complexity Measures in Polynomial Calculus

  2016cites this paper
• A Survey of Proof Complexity from a SAT Solving Perspective

  2015cites this paper
• A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

  2015cites this paper
• On the interplay between proof complexity and SAT solving

  2015cites this paper
• On the Interplay Between Proof Complexity and SAT Solving

  2015cites this paper
• Width Measures for DAGs and Propositional Proof Complexity

  2014cites this paper
• A (Biased) Proof Complexity Survey for SAT Practitioners

  2014cites this paper
• Mini-tutorial on weak proof systems and connections to SAT solving

  2014cites this paper
• The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-algebraic Proofs

  2013cites this paper
• Revisiting Space in Proof Complexity: Treewidth and Pathwidth

  2013cites this paper
• Improved Separations of Regular Resolution from Clause Learning Proof Systems

  2012influential citation
• Proof Complexity of Relativized Statements

  2012cites this paper
• Non-classical Aspects in Proof Complexity

  2012cites this paper
• An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning

  2012influential citation
• Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width

  2011cites this paper
• Parameterized Complexity of DPLL Search Procedures

  2011cites this paper
• A Near-Optimal Separation of Regular and General Resolution

  2011cites this paper
• Optimality of size-degree tradeoffs for polynomial calculus

  2010influential citation
• Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas

  2010cites this paper
• The Strength of Parameterized Tree-like Resolution

  2010cites this paper
• Hardness of Parameterized Resolution

  2010cites this paper
• A simplified way of proving trade-off results for resolution

  2009cites this paper
• An Exponential Lower Bound for Width-Restricted Clause Learning

  2009cites this paper
• Exponential Lower Bounds and Integrality Gaps for Tree-Like Lovász-Schrijver Procedures

  2009cites this paper
• Towards an optimal separation of space and length in resolution

  2008cites this paper
• Short Proofs May Be Spacious : Understanding Space in Resolution

  2008cites this paper
• On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity

  2008cites this paper
• Degree Lower bounds for Algebraic Proof Systems

  2008cites this paper
• Degree lower bounds for a graph ordering principle ∗

  2008cites this paper
• Regular and General Resolution: An Improved Separation

  2008cites this paper
• SAT COMPETITION 2016 Solver and Benchmark Descriptions

  year unknowncites this paper