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.

翻译：我们提出了一种基于弦图的演算方法，用于推理布尔公式的可满足性，并证明其具有可靠性和完备性。随后，我们通过若干案例研究展示该演算的应用：首先分析SAT求解问题，其次研究Horn子句系统，并由此提出一种在Herbrand模型语义下判定命题逻辑程序等价性的新方法。