K. Schütte, “Ein Ansatz zum Entscheidungsverfahren für eine Formelklasse der Prädikatenlogik mit Identität”, Acta Cybern, vol. 4, no. 1, pp. 141-148, Jan. 1978.