On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations
type: Item
instance of: scholarly article
title: On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations
author: Yanyan Li
published in: Annals of Mathematics and Artificial Intelligence
publication date: 2022-11-17T00:00:00Z
Mathematics Subject Classification ID: 90C05
zbMATH DE Number: 7618983
zbMATH Keywords: Horn constraint systems
zbMATH Keywords: cutting plane proofs
zbMATH Keywords: NP-hardness
zbMATH Keywords: soundness and completeness
describes a project that uses: Yices
describes a project that uses: z3
MaRDI profile type: Publication
full work available at URL: s10472-022-09800-7
OpenAlex ID: W4281788412
cites work: Q4218098
cites work: Combining Forward and Backward Abstract Interpretation of Horn Clauses
cites work: Horn Clause Solvers for Program Verification
cites work: Lower bounds for cutting planes proofs with small coefficients
cites work: A combinatorial algorithm for Horn programs
cites work: Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
cites work: On the complexity of cutting-plane proofs
cites work: Automated Reasoning
cites work: Q3224554
cites work: Q4809071
cites work: Outline of an algorithm for integer solutions to linear programs
cites work: The intractability of resolution
cites work: Q4391452
cites work: Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs
cites work: Reducibility among Combinatorial Problems
cites work: Restricted cutting plane proofs in Horn constraint systems
cites work: Finding read-once resolution refutations in systems of 2CNF clauses
cites work: Q5875680
cites work: Q4471290
cites work: Program Development in Computational Logic
cites work: Certifying algorithms
cites work: Q4943600
cites work: Lower bounds for resolution and cutting plane proofs and monotone computations
cites work: Optimal length resolution refutations of difference constraint systems
cites work: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
cites work: Q4539605
cites work: Integral Extreme Points
DOI: 10.1007/S10472-022-09800-7
description: scientific article; zbMATH DE number 7618983