Infinite pseudo-random sequences of high algorithmic complexity Ivan Kramosil, Jan Šindelář (1984) Kybernetika
Introducing general redundancy criteria for clausal tableaux, and proposing resolution tableaux. Kovásznai, Gergely, Kusper, Gábor (2008) Annales Mathematicae et Informaticae