В основе логических систем представления знаний лежит понятие формальной логической системы. Оно является также одним из основополагающих понятий формализации. Основные идеи формализации заключаются в следующем. Вводится множество базовых элементов (алфавит) теории. Определяются правила построения правильных объектов (предложений) из базовых элементов. Часть объектов объявляется изначально заданными и правильными по определению - аксиомами. Задаются правила построения новых объектов из других правильных объектов системы (правила вывода).
Данная схема лежит в основе построения многих дедуктивных СИИ. В соответствии с ней база знаний описывается в виде предложений и аксиом теории, а механизм вывода реализует правила построения новых предложений из имеющихся в базе знаний. На вход СИИ поступает описание задачи на языке этой теории в виде запроса (предложения, теоремы), которое явно не представлено в БЗ, но если оно верно с позиций заложенных в БЗ знаний и не противоречит им, то может быть построено из объектов БЗ путем применения правил вывода. Процесс работы механизма вывода называют доказательством запроса (теоремы). Если запомнить шаги процесса вывода в виде трассы и представить ее пользователю, то она будет объяснением выработанного СИИ решения задачи.
Формальные языки, на которых записываются предложения (формулы) с использованием рассмотренных понятий, получили названия логических языков. С практической и теоретической точек зрения наиболее важными и изученными являются язык логики высказываний и язык логики предикатов. В языке логики высказываний элементарные предложения рассматриваются как неделимые сущности, в языке логики предикатов, наоборот, делается расчленение предложения на субъект и предикат.
В процессе математизации рассуждений различают два вида слов: термы - аналоги имен существительных и формулы - аналоги повествовательных предложений.
Для записи предложений используются стандартные формы высказываний, что даёт возможность, с одной стороны, стандартизовать рассуждения, т.е.