We present a proof procedure based on the KE calculus for propositional logic and its implementation as a short Prolog program. The procedure's time complexity is discussed and compared to that of an efficient Tableau based prover.
Endriss, U. (1999). A time efficient KE based theorem prover. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 313–318). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_27