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 Mlogicq in the file mlogicq.cl contains the syntax of tableau rules for quantifier tableaux.