Proving the infeasibility of Horn formulas through read-once resolution
From MaRDI portal
Publication:6558679
DOI10.1016/J.DAM.2023.02.001MaRDI QIDQ6558679FDOQ6558679
Authors: Piotr Wojciechowski, K. Subramani 
Publication date: 20 June 2024
Published in: Discrete Applied Mathematics (Search for Journal in Brave)
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)
Cites Work
- A Brief Overview of PVS
- Introduction to algorithms
- Title not available (Why is that?)
- Outline of an algorithm for integer solutions to linear programs
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Lower bounds for resolution and cutting plane proofs and monotone computations
- The Complexity of Propositional Proofs
- Lower bounds for cutting planes proofs with small coefficients
- On the complexity of cutting-plane proofs
- The intractability of resolution
- Title not available (Why is that?)
- An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
- Title not available (Why is that?)
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Handbook of automated reasoning. In 2 vols
- Lower bounds to the size of constant-depth propositional proofs
- Title not available (Why is that?)
- Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
- The Complexity of Propositional Proofs
- Redundancy in logic. II: 2CNF and Horn propositional formulae
- Completeness in approximation classes beyond APX
- A combinatorial algorithm for Horn programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Edmonds polytopes and a hierarchy of combinatorial problems. (Reprint)
- The complexity of read-once resolution
- Finding read-once resolution refutations in systems of 2CNF clauses
- Read-once resolutions in Horn formulas
- Copy complexity of Horn formulas with respect to unit read-once resolution
This page was built for publication: Proving the infeasibility of Horn formulas through read-once resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6558679)
