Analyzing read-once cutting plane proofs in Horn systems

DOI10.1007/S10817-022-09618-2MaRDI QIDQ2673307zbMATH OpenOpenAlexWikidataFDO

Authors R. Chandrasekaran, Piotr Wojciechowski, K. Subramani

Publication date 9 June 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-022-09618-2

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Restricted cutting plane proofs in Horn constraint systems
• On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations
• Exact and parameterized algorithms for read-once refutations in Horn constraint systems
• Read-once refutations in Horn constraint systems: an algorithmic approach
• On the complexity of cutting-plane proofs

Cites work

• A combinatorial algorithm for Horn programs
• A framework for the verification of certifying computations
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• Certifying algorithms
• Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs
• Combining forward and backward abstract interpretation of Horn clauses
• Feasibility checking in Horn constraint systems through a reduction based approach
• Finding read-once resolution refutations in systems of 2CNF clauses
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 408798 (Why is no real title available?)
• scientific article; zbMATH DE number 1342249 (Why is no real title available?)
• scientific article; zbMATH DE number 2079335 (Why is no real title available?)
• scientific article; zbMATH DE number 2079347 (Why is no real title available?)
• scientific article; zbMATH DE number 1765669 (Why is no real title available?)
• scientific article; zbMATH DE number 751135 (Why is no real title available?)
• scientific article; zbMATH DE number 1416629 (Why is no real title available?)
• Input Proofs and Rank One Cutting Planes
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• On finding short resolution refutations and small unsatisfiable subsets
• On the complexity of approximating the independent set problem
• On unit read-once resolutions and copy complexity
• Optimal length resolution refutations of difference constraint systems
• Parameterized algorithms
• PRIMES is in P
• Proceedings of the fifth workshop on Horn clauses for verification and synthesis, HCVS 2018, Oxford, UK, July 13, 2018
• Read-once resolutions in Horn formulas
• Reducibility among combinatorial problems
• Restricted cutting plane proofs in Horn constraint systems
• The complexity of read-once resolution
• The intractability of resolution
• Theory and Applications of Satisfiability Testing
• What is answer set programming to propositional satisfiability

Cited in

(3)

• Exact and parameterized algorithms for read-once refutations in Horn constraint systems
• Integer feasibility and refutations in UTVPI constraints using bit-scaling
• Read-once refutations in Horn constraint systems: an algorithmic approach

This page was built for publication: Analyzing read-once cutting plane proofs in Horn systems

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