Literature.
[1] Ján Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
[3] Ján Komara. Recursive Functions. Online.
[CL] Remark. The module Mlogicp in the file mlogicp.cl contains the syntax of propositional tableau rules.