Copy complexity of Horn formulas with respect to unit read-once resolution

DOI10.1016/J.TCS.2021.08.017MaRDI QIDQ2235734zbMATH OpenOpenAlexWikidataFDO

Authors Piotr Wojciechowski, K. Subramani

Publication date 21 October 2021

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

Full work available at URL https://doi.org/10.1016/j.tcs.2021.08.017

zbMATH Keywords

copy complexityproof systemread-onceresolutionunit read-once

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Read-once resolutions in Horn formulas
• On unit read-once resolutions and copy complexity
• On the copy complexity of width 3 Horn constraint systems
• Complexity of the problem of being equivalent to Horn formulas
• Automated Deduction – CADE-20
• Complexity of the problem of being equivalent to Horn formulas. II
• scientific article; zbMATH DE number 4085614
• On the computational complexity of read once resolution decidability in 2CNF formulas
• Exact and parameterized algorithms for read-once refutations in Horn constraint systems
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation

Cites work

• A continuous–discontinuous second‐order transition in the satisfiability of random Horn‐SAT formulas
• A Machine-Oriented Logic Based on the Resolution Principle
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• Answer set programming
• Combining forward and backward abstract interpretation of Horn clauses
• Finding read-once resolution refutations in systems of 2CNF clauses
• Handbook of automated reasoning. In 2 vols
• HoIce: an ICE-based non-linear Horn clause solver
• scientific article; zbMATH DE number 4147465 (Why is no real title available?)
• scientific article; zbMATH DE number 3782373 (Why is no real title available?)
• scientific article; zbMATH DE number 1179974 (Why is no real title available?)
• scientific article; zbMATH DE number 1361489 (Why is no real title available?)
• scientific article; zbMATH DE number 1368924 (Why is no real title available?)
• Learning conjunctions of Horn clauses
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Lower bounds for resolution and cutting plane proofs and monotone computations
• On unit read-once resolutions and copy complexity
• Read-once resolutions in Horn formulas
• Reducibility among combinatorial problems
• SMT-based model checking for recursive programs
• The complexity of finding read-once NAE-resolution refutations
• The complexity of read-once resolution
• The Decision Problem for a Class of First‐Order Formulas in Which all Disjunctions are Binary
• The intractability of resolution
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Verifying Array Programs by Transforming Verification Conditions
• Why Horn formulas matter in computer science: initial structures and generic examples

Cited in

(4)

• Read-once resolutions in Horn formulas
• Theory and Applications of Satisfiability Testing
• Farkas Bounds on Horn Constraint Systems
• Proving the infeasibility of Horn formulas through read-once resolution

This page was built for publication: Copy complexity of Horn formulas with respect to unit read-once resolution

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