Komara, J. : Efficient elimination of Skolem functions in LKh.odkaz
Buss, S.R. : An introduction to proof theory.
Hähnle, R., Schmitt, P.H. : The liberalized delta-rule in free variable semantic tableaux.
Švejdar, V. : Logika Neúplnost, složitost a nutnost.Praha: Academia, 2002.ISBN
80-200-1005-X
Barwise, J. : An introduction to first-order logic. In: J. Barwise (ed.) Handbook of Mathematical Logic,pp. 5–46. North-Holland (1977)
Schwichtenberg, H. : Proof theory: Some applications of cut-elimination. In: J. Barwise (ed.) Hand-book of Mathematical Logic, pp. 867–912. North-Holland (1977)
Takeuti, G. : Proof Theory, 2nd edn. North-Holland, Amsterdam (1987)
Troelstra, A.S., Schwichtenberg, H. : Basic Proof Theory, second edition. Cambridge Tractsin Theoretical Computer Science. Cambridge University Press (2000)
R Kent Dybvig. The Scheme programming language. Mit Press, 2009. odkaz
Ján Kľuka a Jozef Šiška: Prednášky z kurzu matematika 4, 2020.
Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli
Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. The racket manifesto. In 1st
Summit on Advances in Programming Languages (SNAPL 2015). Schloss Dagstuhl-
Leibniz-Zentrum fuer Informatik, 2015. odkaz
J. Komara and P. J. Voda. Syntactic reduction of predicate tableaux to propositional
tableaux. In Proceedings of TABLEAUX ’95, number 918 in LNAI, pages 231–246.
Springer Verlag, 1995.