Unit refutability of Horn constraint systems -- certification and parallel complexity

DOI10.1016/J.TCS.2025.115419MaRDI QIDQ6930241zbMATH OpenFDO

Authors Piotr Wojciechowski, K. Subramani

Publication date 16 September 2025

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.TCS.2025.115419

Mathematics Subject Classification ID

Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Parallel algorithms in computer science (68W10)

Cites work

• A combinatorial algorithm for Horn programs
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• Analyzing unit read-once refutations in difference constraint systems
• Automated Reasoning
• Extended Horn sets in propositional logic
• Finding read-once resolution refutations in systems of 2CNF clauses
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 176740 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1324220 (Why is no real title available?)
• scientific article; zbMATH DE number 1738295 (Why is no real title available?)
• scientific article; zbMATH DE number 1368924 (Why is no real title available?)
• scientific article; zbMATH DE number 2090312 (Why is no real title available?)
• scientific article; zbMATH DE number 784042 (Why is no real title available?)
• Input Proofs and Rank One Cutting Planes
• Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
• Linear and unit-resulting refutations for Horn theories
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• On finding solutions for extended Horn formulas
• On the complexity of cutting-plane proofs
• Optimal length resolution refutations of difference constraint systems
• Outline of an algorithm for integer solutions to linear programs
• Refutation search for Horn sets by a subgoal-extraction method
• Renaming a Set of Clauses as a Horn Set
• Restricted cutting plane proofs in Horn constraint systems
• Semantic Resolution for Horn Sets
• The arborescence-realization problem
• The complexity of read-once resolution
• The intractability of resolution
• The Unit Proof and the Input Proof in Theorem Proving
• Theorie der einfachen Ungleichungen.
• Tree-like unit refutations in Horn constraint systems
• Two variables per linear inequality as an abstract domain
• Unit Refutations and Horn Sets
• Unit refutations in Horn constraint systems
• Visible Structures in Number Theory
• What is answer set programming to propositional satisfiability

This page was built for publication: Unit refutability of Horn constraint systems -- certification and parallel complexity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6930241)