Статья 544

Определим язык.
Алфавит.
множество пропозициональных переменных.
логические связки.
операторы верификации с ресурсами.
Всякая пропозициональная переменная является формулой.
ЕСЛИ А И В - формулы, то и А, АВ - формулы.
Ничто другое формулой не является. Формулы вида читаются верифицируема за время. Связка эквивалентности вводится по определению обычным образом.
Модель
Моделью будем называть пару, где истинностная оценка пропозициональных переменных - оценка ресурсов.
Для и выполняются условия и для всякого имеет место.
Обе оценки по индукции распространим на множество всех формул следующим образом, в противном случае.
Формула 4 истинна в модели если и только если. Формула А общезначима, если и только если она истинна во всех моделях. Класс общезначимых формул аксиоматизируем посредством аксиом и правил вывода классической логики высказываний плюс следующих аксиом
Почти во всех языках программирования имеются логические выражения, которые используются в основном для управления ходом выполнения программ.