1964 йылда Ленинград логика белгесе Сергей Масловтың «Предикаттарҙың классик иҫәпләүендә сығарылмалыҡты асыҡлауҙың кире ысулы» («Обратный метод установления выводимости в классическом исчислении предикатов») эше баҫылып сыға, унда беренсе тапҡыр предикация иҫәпләүендә теоремаларҙы иҫбатлауҙы автоматик эҙләү ысулы тәҡдим ителә.