On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations
From MaRDI portal
Publication:2095546
DOI10.1007/s10472-022-09800-7OpenAlexW4281788412MaRDI QIDQ2095546
Publication date: 17 November 2022
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-022-09800-7
Uses Software
Cites Work
- Certifying algorithms
- On the complexity of cutting-plane proofs
- Optimal length resolution refutations of difference constraint systems
- Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs
- The intractability of resolution
- Finding read-once resolution refutations in systems of 2CNF clauses
- Restricted cutting plane proofs in Horn constraint systems
- A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
- A combinatorial algorithm for Horn programs
- Horn Clause Solvers for Program Verification
- Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
- Outline of an algorithm for integer solutions to linear programs
- Lower bounds for cutting planes proofs with small coefficients
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Reducibility among Combinatorial Problems
- Combining Forward and Backward Abstract Interpretation of Horn Clauses
- Automated Reasoning
- Integral Extreme Points
- Program Development in Computational Logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item