A Complete Diagrammatic Calculus for Boolean Satisfiability

作     者：Gu, Tao Piedeleu, Robin Zanasi, Fabio 

作者机构：University College London United Kingdom 

出 版 物：《arXiv》 (arXiv)

年 卷 期：2022年

核心收录：

主　　题：Logic programming 

摘      要：We propose a calculus of string diagrams to reason about satisfiability of Boolean formulas, and prove it to be sound and complete. We then showcase our calculus in a few case studies. First, we consider SAT-solving. Second, we consider Horn clauses, which leads us to a new decision method for propositional logic programs equivalence under Herbrand model semantics. © 2022, CC BY.