DCG LaTeX printer for FOL prover The following SWI Prolog code is mainly Jens Ottens’ leanseq.pl prover for classical FOL:
