Another sequent calculus prover in Prolog: leanseq.pl
2021-12-03, updated 2021-12-03 next - previous
A note about the prover published by Philip Zucker from Jens Otten’s lectures.
The following Prolog code can be considered as an implementation of Wang’s algorithm [1]
[1]
H. Wang, “Toward mechanical mathematics,” Ibm j. res. dev., vol. 4, no. 1, pp. 2–22, Jan. 1960 [Online]. Available: https://doi.org/10.1147/rd.41.0002