4
$\begingroup$

One of the more common ways to do proofs is using a deductive system.

Can proofs instead be done using graphs?

I am seeking papers that outline from the ground up how such a system works. If example code in Prolog is provided even better.

This question originated from using Incredible Proof Machine and looking at the code and reading the paper.

such a graph constitutes a rigorous, formal proof.

While I can Google for words such as "proof", "graph", "deductive system", such results do not outline a path for understanding and building such a system; the results are more like throwing darts and randomly hitting spots on the target.

EDIT

Before asking this question, this was one of the better papers I found Proofs with graphs. I am hoping for something that is more basic with code examples.

Keywords:

  • Deduction Graphs
  • Proof Nets
  • Natural Deduction
  • Cut-elimination
  • Lambda Calculus with Let-binding
  • Typed Lambda Calculus
Improve this question
$\endgroup$
4
  • $\begingroup$ Perhaps you're looking for proof nets? I don't know enough about them to write up an answer, though. $\endgroup$
    – James Martin
    Commented Feb 28, 2022 at 17:10
  • $\begingroup$ Something like: en.wikipedia.org/wiki/Cirquent_calculus or arxiv.org/abs/1007.0725 ? $\endgroup$
    – Rob
    Commented Mar 1, 2022 at 11:42
  • $\begingroup$ Of interest: Cirquent Calculus in a Nutshell (pdf - preprint) by Giorgi Japaridze $\endgroup$
    – Guy Coder
    Commented Mar 1, 2022 at 12:27
  • $\begingroup$ Of interest: Giorgi Japaridze Research $\endgroup$
    – Guy Coder
    Commented Mar 1, 2022 at 12:29

2 Answers 2

Reset to default
5
$\begingroup$

Well, a proof engine is built atop a proof calculus, right? And natural deduction basically amounts to using a specific set of possible labeled edges in graphs for proofs (namely, introduction and elimination rules). There's a couple papers summarizing this very aspect of natural deduction:

  • Herman Geuvers and Iris Loeb, "Natural Deduction via Graphs: Formal Definition and Computation Rules". Mathematical Structures in Computer Science 17 no.3 (2007) pp.485-526; doi:10.1017/S0960129507006123 Eprint
  • Willem Heijltjes, "Graph Rewriting for Natural Deduction and the Proper Treatment of Variables". Masters thesis, Eprint

From another perspective, we could look at proofs in terms of strict monoidal categories (glorified graphs!), which has been discussed in:

  • Manuel G. Clavel and Jose Meseguer, "Axiomatizing Reflective Logics and Languages". Eprint (pdf)

As far as, you know, actually building a proof engine based on these ideas...well, I guess that's left as an exercise for the reader ;)

Improve this answer
$\endgroup$
1
  • $\begingroup$ @GuyCoder It dawns on me also that Freek Wiedijk's implementation of Automath uses pointers in a clever way that form a graph (as discussed briefly in section 4.2 of his paper). Since proof objects are terms, this may be interesting to you; but this is not directly relevant, so I mention it as an aside in this comment. $\endgroup$
    – Alex Nelson
    Commented Mar 4, 2022 at 16:34
9
$\begingroup$

Your question is quite vague, but can be answered positively when taken literally. Indeed, most implementations of a deductive system are actually already using graphs internally.

When phrased mathematically a proof is an inductively defined tree. But in a proof assistant, they are typically represented in memory as some variant of algebraic datatypes (if the implementation language is ML-like) or a bunch of pointers between structs meant to encode them (if the language is lower-level). Now, in order to reduce the memory consumption, programs performing symbolic computations often rely on the process of hashconsing. Without entering the details, this allows sharing the structurally equivalent subtrees of the proof as literally the same object in memory. At that point, your proof is not a tree anymore but a DAG.

This may even be reflected in the surface language. For instance, the Coq tactic engine relies on the so-called evar calculus, which is just a fancy name for a higher-level notion of heap and pointers. Using evars as pointers, you can actually share subproofs across different places of the derivation.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ I have added two papers in the answer. There is not a wealth of papers in this area since it is right at the intersection of very practical considerations and folklore. $\endgroup$
    – Pierre-Marie Pédrot
    Commented Feb 28, 2022 at 10:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.