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