Equilibrium graphs (Q2317964)

Existential graphs (EGs) are a graphical representation of formulas of first-order logic introduced by Charles Sanders Peirce. EGs have constructs for conjunction, negation and existential quantifiers, while disjunction, implication and universal quantification are derived using first-order equivalences. It turns out that EGs are not well-suited for non-classical logics, among them answer set programming (ASP) and its logical formalization in terms of equilibrium logic. In order to extend EGs to ASP, the authors of this article suggest a new construct to properly represent implications, and also propose a new way to use EGs constructs to properly represent universal quantification. The resulting graphical system is called equilibrium beta graph. Without going in too much details, EGs represent formulas using predicate names, closed curves to denote negation, implicit conjunction of any subformula in the graph, and lines connecting predicate names to join arguments (as an alternative to first-order variables). Hence, lines crossing closed curves represent universal quantifications, while a disjunction can be represented by applying De Morgan's laws in terms of closed curves (and implicit conjunction). Similarly, the representation of an implication is obtained by using the equivalence \(\phi \rightarrow \psi \equiv \neg\phi \vee \psi\), and then by representing the disjunction in terms of closed curves (and implicit conjunction). It turns out that (first-order) equivalent formulas like \(\mathit{rains} \rightarrow \mathit{wet} \vee \mathit{umbrella}\), \(\mathit{rains} \wedge \neg \mathit{wet} \rightarrow \mathit{umbrella}\), and \(\mathit{rains} \wedge \neg \mathit{umbrella} \rightarrow \mathit{wet}\) are all representable as \(\neg(\mathit{rains} \wedge \mathit{wet} \wedge \neg\mathit{umbrella})\), which is possibly an issue for readability and certainly a problem for ASP, where such formulas are not equivalent. The extension to EGs proposed by the authors of this article is to use a different construct for \textit{consequences} of implications. Such a construct is a rectangle enclosing each disjunct in the consequence of an implication, and is also used together with lines to provide an explicit representation for universal quantifications. The fact that rectangles in the same area are implicitly interpreted as a disjunction is particularly convenient for ASP, where rules are implications comprising a conjunction of literals in their antecedents, and a disjunction of literals in their consequences. Details of the proposed extension are given in the article, which is a nice reading with a clear structure and narrative. The many examples provided by the authors ease the understanding of the issues with the original graphical system, and clarify the design choices of the proposed extension. The article also shows an algorithm to transform an equilibrium beta graph in the corresponding first-order formula, and outlines possible future extensions to accommodate other common constructs of ASP.