I'm searching for some software or open source project which is able to prove propositions of predicate logic of first order in the way of natural deduction introduced for example in the book of Lemmon (beginning logic) and can put the results in LaTeX code.


(You can find a short introduction [here](https://plato.stanford.edu/entries/natural-deduction/).)



Software to prove statements in the way of natural deduction (tabular form introduced by Lemmon)
Here are two tools for teaching natural deduction proofs that were developed in London in the 1990s.


**Jape**


Developed by
[Bernard Suffrin](http://www.cs.ox.ac.uk/bernard.sufrin/personal/), at Worcester College Oxford, and
[Richard Bornat](http://www.eis.mdx.ac.uk/staffpages/r_bornat/), formerly at Queen Mary and now at Middlesex.


[Downloads and source code at GitHub](https://github.com/RBornat/jape)


**Pandora**


[Main page](https://www.doc.ic.ac.uk/pandora/) orginally developed by students at Imperial College in connection with a course taught by [Krysia Broda](http://wp.doc.ic.ac.uk/kb/teaching/) and others.


**Proof boxes in LaTeX**


I forgot to mention my own work! This is not a piece of software of the above kind, but a way of typesetting box-style natural deduction proofs in LaTeX.


[My LaTeX macros](http://paultaylor.eu/proofs/)


