A Complete Diagrammatic Calculus for Boolean Satisfiability
Logic in Computer Science
2023-06-22 v5
Abstract
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.
Cite
@article{arxiv.2211.12629,
title = {A Complete Diagrammatic Calculus for Boolean Satisfiability},
author = {Tao Gu and Robin Piedeleu and Fabio Zanasi},
journal= {arXiv preprint arXiv:2211.12629},
year = {2023}
}