Tao Gu ; Robin Piedeleu ; Fabio Zanasi - A Complete Diagrammatic Calculus for Boolean Satisfiability

entics:10481 - Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII - https://doi.org/10.46298/entics.10481
A Complete Diagrammatic Calculus for Boolean SatisfiabilityArticle

Authors: Tao Gu ; Robin Piedeleu ; Fabio Zanasi

    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.


    Volume: Volume 1 - Proceedings of MFPS XXXVIII
    Published on: February 22, 2023
    Accepted on: December 15, 2022
    Submitted on: December 14, 2022
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 369 times.
    This article's PDF has been downloaded 203 times.