Questions tagged [proof-tree]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
-3 votes
1 answer

Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?

So I'm not sure how things are done in Lean4 or Coq, but I'm interested in their search features. For example, "Search for all theorems that get satisfied given a user-defined list of ...
D Left Adjoint to U's user avatar
5 votes
0 answers

Display style proofs using Coq

How to display proofs using in Gentzen tree style and (or) Fitch-style, using CoqIDE or JsCoq? PS: I'm rookie used coq.
Valdigleis's user avatar