В дисертації автором побудовані методи пошуку виведення в класичній логіці першого порядку, які можуть бути використані в системах логічного програмування, та їх теоретичному дослідженню на коректність і повноту, де коректність і повнота розуміються в логічному сенсі. Для логіки без рівності розроблено секвенційний підхід до встановлення вивідності, що дав змогу довести секвенційну форму теореми Ербрана, яка не потребує проведення попередньої сколемізації. Це дає основу для побудови сімейства коректних і повних, в загальному випадку, числень секвенційного типу для пошуку виведення в сигнатурі вихідної теорії першого порядку. Використовуючи її, доводиться повнота цілеорієнтованого числення такого типу. Побудовано та досліджено на коректність і повноту числення літеральних секвенцій і числення літеральних дерев у випадку відсутності рівності. Встановлено зв'язок цих числень із запропонованими модифікаціями відомих резолюційних методів таких, як SLD-резолюція, лінійна і вхідна резолюції, та метод елімінації моделей. Використовуючи її, доведено коректність і повноту цих модифікацій. Це дозволяє будувати повні розширення дедуктивного апарату певних інтелектуальних систем, включаючи системи логічного програмування. Для класичної логіки з рівністю побудовано пара модуляційні розширення числення літеральних дерев, а також модифікації резолюційних методів і стратегій, включаючи SLD-резолюцію, вхідну резолюцію, лінійну резолюцію і метод елімінації моделей. Доведено їх коректність и повнота у випадку використання аксіом функціональної рефлективності і показана неможливість отримання повноти без цих аксіом.