Лекция 9: метод резолюций в исчислении предикатов

VI. Раскрытие информации в бухгалтерской отчетности

См. схему "Информация об основных средствах, подлежащая раскрытию в учетной политике"

Приказом Минфина РФ от 12 декабря 2005 г. N 147н в пункт 32 настоящего Положения внесены изменения, вступающие в силу начиная с бухгалтерской отчетности 2006 г.

См. текст пункта в предыдущей редакции

32. В бухгалтерской отчетности подлежит раскрытию с учетом существенности как минимум следующая информация:

о первоначальной стоимости и сумме начисленной амортизации по основным группам основных средств на начало и конец отчетного года;

о движении основных средств в течение отчетного года по основным группам (поступление, выбытие и т.п.);

о способах оценки объектов основных средств, полученных по договорам, предусматривающим исполнение обязательств (оплату) неденежными средствами;

об изменениях стоимости основных средств, в которой они приняты к бухгалтерскому учету (достройка, дооборудование, реконструкция, частичная ликвидация и переоценка объектов);

о принятых организацией сроках полезного использования объектов основных средств (по основным группам);

об объектах основных средств, стоимость которых не погашается;

об объектах основных средств, предоставленных и полученных по договору аренды;

об объектах основных средств, учитываемых в составе доходных вложений в материальные ценности;

о способах начисления амортизационных отчислений по отдельным группам объектов основных средств;

об объектах недвижимости, принятых в эксплуатацию и фактически используемых, находящихся в процессе государственной регистрации.

Вспомним, как решается задача вывода в исчислении высказываний:

1. вывод Ф₁, Ф₂,..., Ф_n |– Q заменяется на доказательство методом от противного– Ф₁, Ф₂,..., Ф_n, ØQ |–

2. Все формулы Ф_i приводятся к нормальной конъюнктивной форме – Ф₁ = D₁ & D₂ &... & D_n,.

3. Выписывается множество дизъюнктов D_ij, состоящих только из положительных и отрицательных литералов D_ij = L₁ V L₂ V...

4. Применяется правило резолюции

A V B, C V ØB
A V C

до тех пор, пока не получен пустой дизъюнкт.

Здесь:

D₁= A V B; D₂= C V ØB - родительские предложения

D₃= A V C - резольвента

В исчислении предикатов сущность метода остается прежней, но появляются особенности, связанные с наличием кванторов и переменных.

Алгоритм приведения формул к виду, пригодному для доказательства методом резолюции в исчислении предикатов.

1. Перенести заключение в посылку с отрицанием Ф₁, Ф₂,..., Ф_n, ØQ |–

2. Во всех формулах исключить эквивалентности, используя равенство
AºB = (A É B) & (B É A)

3. Во всех формулах исключить импликации, используя равенство
A É B = ØA V B

1. Продвинуть внутрь формул знак отрицания, используя формулы де–Моргана. В сложных выражениях лучше начинать с внешних знаков отрицания, т.к. внутренние могут сократиться и сэкономить работу.
   Ø(A V B) = Ø A & ØB Ø(A & B) = Ø A V ØB
   Ø x A(x) = x ØA(x) Ø x A(x) = x ØA(x)
2. Исключить кванторы существования x P(x, y)
3. Раскрыть конъюнкции, попавшие внутрь дизъюнкций, используя дистрибутивный закон
   P V (Q & R & …) = (P V Q) & (P V R)...
4. Выносим все кванторы всеобщности с переименованием переменных (если это необходимо). Здесь уместно провести аналогию с локальными переменными. Локальную переменную можно заменить на любую другую, лишь бы не возникало коллизий (совмещения) с другими переменными в той же самой области действия
   

x (rod(x,y), m(x) É father(x,y) Þ x₁ (rod(x₁,y₁), m(x₁) É father(x₁,y₁)
x (rod(x,y), f(x) É mother(x,y) Þ x₂ (rod(x₂,y₂), f(x₂) É mother(x₂,y₂)

1. Выписываем все дизъюнкты
2. Применяем правило резолюции, до получения пустого дизъюнкта. Для совпадения литералов применяем подстановку и унификацию.

Рассмотрим более подробно шаги 5 и 9, т.к. они непосредственно связаны с наличием кванторов и переменных.

Дата добавления: 2014-01-07