This tool provides autocompletion of justifications for Fitch- and (output-only) Gentzen-style first-order natural deduction, in a language without function symbols.
Specifically, given a (structured) array of formulas, it finds justifications for these formulas, if there are any.
Rendered deductions are printed as HTML and LaTeX, using either Fitch- or Gentzen-style.
Please see help for more information.
URL of a running instance is live-updated with state; so to share your proofs, just copy-paste the URL.