Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2



страница3/5
Дата02.01.2013
Размер0.5 Mb.
ТипДокументы
1   2   3   4   5

Пример 3. Пусть нам предъявлена формула ((pq)&(pq))(p(q&p))

Далее действуем согласно нашей процедуре.

  1. Располагаем формулу внизу предполагаемого вывода и находим ее главный знак.


Формула имеет вид АВ, где А -это ((pq)&(pr)), а В -это (p(q&r)). Следовательно, на предыдущем шаге вывод имел вид:

.


  1. Формула p(q&r) имеет вид АВ, где А - это p, а В - это q&r. Следовательно, вывод на предыдущем шаге имел вид:


Формулу q&r можно получить с помощью фигуры заключения и, возможно, что на предыдущем шаге вывод имел вид:



Этот шаг требует подробного разъяснения. Прежде заметим, что

переход от части вывода к части вывода &+, вообще говоря, не является очевидным для NJ-исчисления. Почему мы не предположили, что предыдущий шаг-это применение фигуры заключения ? Тогда часть вывода, обозначенная нами как &+ , имела бы вид:

ВПВ.

И почему предыдущий шаг не является применением фигуры заключения - или - и, вообще, одной из тех фигур заключения, допущения которых не входят в нижнюю формулу в качестве подформул?

Указанная часть вывода могла бы иметь вид:

или и т.п., где А и В неизвестные на этом шаге формулы. Этот же самый вопрос мы могли задать и раньше, рассматривая пример 2, на том шаге, на котором мы переходим от формулы r к поиску ее вывода из допущений, но в том случае мы решили не усложнять изложение доказательства. Заметим, что, как и формула r из примера 2, так и формула q&r из примера 3, обе являются "пограничными" формулами. Они делят вывод на две части (см.стр.
18), а сам поиск вывода - на два этапа (здесь мы подразумеваем, что вывод строиться снизу вверх):

1 этап. Анализ заданной формулы, нахождение допущений и определение "пограничной" формулы; наши действия на этом этапе полностью определяются структурой заданной формулы. Первый этап является подготовительным этапом. Можно сказать, что здесь мы формулируем условие задачи, т.е. определяем структуру заданной формулы, допущения и "пограничную" формулу.

2 этап. Поиск вывода "пограничной" формулы из выявленных допущений; наши действия на этом этапе, в общем случае, не определены. (На втором этапе мы приступаем к решению задачи, т.е. пытаемся ответить на вопрос: можно ли из данных допущений получить "пограничную" формулу или нет).
Неопределенность действий на втором этапе связана с наличием фигур заключения, не содержащих допущения в качестве подформул нижней формулы и при построении снизу вверх, мы непосредственно не могли бы усмотреть дальнейшие шаги, если бы на первом этапе не составили список допущений. Именно поэтому для нас важно при анализе заданной формулы представить общий вид доказательства, примиряясь с наличием не заполненной части вывода. Более того, формирование общего вида доказательства является важным эвристическим принципом, помогающим нам осуществить поиск доказательства.
Вернемся к рассмотрению примера 3. Пусть формула q&r является "пограничной" формулой, а формулы (pq)&(pr) и p - допущениями. Возникает вопрос: все ли допущения определены на данном этапе? Почему, например, мы не вносим в список допущений формулы q и r, являющимися верхними формулами фигуры заключения &+ предполагаемого вывода?

Предположим, что формулы q и r - допущения. Тогда список допущений будет выглядеть:

Заметим, что при применении фигуры заключения &+ мы не отбрасываем допущений, это можно сделать применением одной из следующих фигур заключения: +, -, +, -. Тогда какой-то участок вывода содержал бы , например, такую часть:

Однако доказываемая нами формула не содержит подформулы q(r(q&r)). Следовательно, формулы q и r не являются допущениями. Далее, если формулы q и r не допущения, то они являются нижними формулами разных ветвей некоторой части общего вывода. Причем и q, и r должны быть получены из допущений (pq)&(pr) и p. Проверим наше предположение.

Заметим, что q и r являются подформулами формулы (pq)&(pr) и "добраться" до q мы могли бы применением фигуры заключения -при наличии формулы pq и допущения p. Тогда эта часть вывода имела бы вид:



В свою очередь, формулу pq можно получить, применяя фигуру заключения &- к формуле (pq)&(pr), тогда часть вывода до q будет иметь вид:

Аналогично, для части вывода до формулы r.
.
Теперь восстанавливаем общий вывод:

Итак, все допущения отброшены и вывод построен.

***

Пример 4. Дана формула (pq)(qp). Эта формула выражает коммутативность дизъюнкции. Действуем согласно нашей процедуре.

1.Располагаем формулу внизу предполагаемого вывода и находим ее главный знак.


Формула имеет вид: АВ, где А - это pq, а В - это qp.

2. Тогда на предыдущем шаге вывод имел вид:


***

Прежде чем построить вывод данной формулы мы хотели бы внести дополнения в терминологию. До сих пор, характеризуя формулы, входящие в вывод, мы использовали термины "допущение" и "пограничная формула". Этим терминам соответствуют термины "антецедент" и "консеквент", введенные в параграфе 18 второй главы настоящего учебника и характеризующие структуру формул с точки зрения кратной импликации. В дальнейшем термин "антецедент" мы будем использовать как синоним термина "допущение", а термин "консеквент" мы будем использовать как синоним термина "пограничная формула".

***
Итак, формула pq является допущением [антецедентом формулы (pq)(qp) ] предполагаемого вывода, а формула qp - "пограничной" формулой [(консеквентом формулы (pq)(qp)] этого вывода. Хотя структура доказываемой формулы (pq)  (qp) проста, но пока не ясно, как, используя единственное допущение, получить формулу qp.

Прежде заметим, что допущение имеет вид АВ. Это наводит на предположение о том, что консеквент можно получить применением фигуры -. Напишем ее еще раз.
.
Попробуем восстановить общий вид вывода нашей формулы согласно указанной схеме:

.
Рассмотрим получившуюся ситуацию. В схеме фигуры заключения - мы вписали формулу pq вместо выражения АВ, вместо С - формулу qp, вместо А - p , а вместо В - q. Допущения +2 и +3 мы можем ввести в вывод, не нарушая структуры конечной формулы, потому, что применение фигуры - позволяет их отбрасывать.

Теперь перейдем к частям вывода и . И в том и другом случае часть вывода, обозначенная посредством выражения , восстанавливается непосредственным применением фигуры заключения +. Таким образом, результирующий вывод будет иметь вид:

.
Вывод построен.

***

Пример 5. Пусть дана формула (pq)((pr)(qr)).

Первый этап.

1. Располагаем формулу внизу предполагаемого вывода и определяем главный знак:



2. Тогда на предыдущем шаге вывод имел вид:



  1. И, завершая анализ заданной формулы, приходим к следующей ситуации:


Второй этап.

Далее рассуждаем следующим образом. Консеквент имеет вид АВ, следовательно, на каком-то шаге мы, вероятно, должны будем использовать фигуру заключения +. Допущения имеют вид АВ и АВ, следовательно, в процессе построения вывода нам, вероятно, понадобится использовать фигуры заключения - и -. Затем, поскольку мы предполагаем использовать фигуру заключения -, то согласно схеме для этой фигуры вместо АВ берем pr, вместо А - p, а вместо В - r. Формула С - это qr.

4. И теперь восстановленная часть вывода имеет вид:



Далее рассуждаем так: формула qr записана над чертой дважды и, согласно фигуре заключения -, эта формула должна быть получена из допущений p и r, с использованием, быть может, еще других допущений. Замечаем, что одно из вхождений в вывод формулы qr получается из r непосредственным применением фигуры заключения +, т.е.:

Другое вхождение формулы qr можно получить из двух допущений pq и p, а именно:

5. И теперь, суммируя вышесказанное, завершаем построение основного вывода:

.
***
Подведем некоторые итоги. При рассмотрении примеров 3,4 и 5 мы обнаружили, что в выводе кроме явных допущений, определяемых в процессе анализа заданной формулы, можно использовать дополнительные допущения, но только такие, которые отбрасываются внутри вывода и не оказывают влияния на структуру заданной формулы (т.е. не входят в конечную формулу в качестве подформул).

***
Пример 6. Пусть дана формула (p&p).
Этот случай подводит нас к рассмотрению косвенных доказательств. Как известно из курса традиционной логики, существует два вида доказательств: прямые и косвенные. Косвенные доказательства в свою очередь также делятся на два вида: апагогические и разделительные. Особенностью апагогического доказательства является то, что в нем используется в качестве одного из аргументов суждение, противоречащее тезису доказательства, т.е. антитезис. Доказательство тезиса строится через отрицание антитезиса. Схема этого доказательства такова:


В исчислении NJ нет фигуры заключения "Удаление двойного отрицания", поэтому Генцен для формализации выводов, аналогичных косвенному доказательству, вводит две фигуры заключения для знака отрицания: фигуру заключения "Введение отрицания":

и фигуру заключения "Удаление отрицания":
.
Теперь апагогическое доказательство для исчисления NJ можно представить в виде трех схем:

или , или

Заметим, что для этих схем в фигуре заключения "Удаление отрицания" мы заменили символы А и А на В и В соответственно. Выражение означает, что на этом шаге мы отбрасываем допущение А. В конкретном выводе мы записали бы, например: "-1".

Что касается разделительного косвенного доказательства, то его схема по форме совпадает с модусом tollendo ponens. Схему этого доказательства для NJ-исчисления можно представить в виде:

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

Вернемся к нашему примеру. Главным знаком формулы (p&p) является знак "". Следовательно, вывод этой формулы должен завершаться применением фигуры "Введение отрицания".

1. Располагаем нашу формулу внизу предполагаемого вывода:

.
2. Тогда на предыдущем шаге вывод имел вид:

сравните со схемой ;
где формула p&p взята вместо А.

3. Формулу Л можно получить только применением фигуры "Удаление отрицания", и, следовательно, на предыдущем шаге вывод имел вид:

.

***

Примечание 1. Формулу Л можно рассматривать как допущение фигуры , и тогда предполагаемый вывод выглядел бы так:

.

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

.
Формула Л(p&p) - выводима в NJ-исчислении, но мы то хотели доказать выводимость другой формулы. Следовательно, формулу "Л" нельзя рассматривать как допущение.

Примечание 2. Часть нашего рассуждения, начинающаяся со слов: "…и следовательно, на предыдущем шаге вывод имел вид:

.
также требует разъяснения. Здесь может возникнуть вопрос: "Почему над формулой Л мы записали формулы p и p, а не какие либо другие формулы, что не противоречило бы общей схеме косвенного доказательства? Дело в том, что мы сообразуем построение вывода с теми допущениями, которые выявляются при анализе формулы. В данном случае мы замечаем, что из формулы p&p можно получить применением фигуры "удаление конъюнкции" как формулу p, так и формулу p.

5. Итак, в окончательном виде вывод записывается следующим образом:

.

***
Пример 7. Пусть дана формула ((p&q)r)((pr)(p&q)) и нам необходимо построить ее вывод. Действуем стандартным образом.

Первый этап.

  1. Располагаем формулу внизу предполагаемого вывода:



2. Замечаем, что два первых шага - это применение фигуры заключения +:

.
3. Формула (p&q) является пограничной формулой вывода (консеквентом конечной формулы). Это означает, что все другие допущения (кроме допущений +1 и +2), которые появятся в выводе, должны быть отброшены с помощью фигур заключения, расположенных в выводе выше данной формулы. Далее рассуждаем следующим образом. Главный знак формулы (p&q) - отрицание. Следовательно, на предыдущем шаге вывод имеет вид:

,
где формула (p&q) - допущение косвенного доказательства.
Второй этап.

Следующие шаги очевидны и вывод восстанавливается без комментариев.


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

Пример 8. Пусть дана формула ((pp)p)(qp). Действуем согласно стандартной процедуре.

Первый этап.

  1. Располагаем формулу внизу предполагаемого вывода:




  1. Далее вывод будет иметь вид:

.
Второй этап.

  1. Анализируем создавшуюся ситуацию. Вывод содержит "пограничную" формулу qp и единственное допущение (pp)p. Формула (pp)p имеет вид АВ, где А - это формула (pp), а В - это формула p. Заметим, что вывести "пограничную" формулу непосредственно из допущения мы не можем. Также нельзя ввести и допущения, которые сопоставляются фигурам заключения - или +, так как у нас нет допущения, содержащего знак , а пограничная формула не содержит знака . Первое впечатление таково, что данную формулу вывести невозможно. Тем не менее мы не оставляем попыток построить вывод.

Во-первых, замечаем, что формулу qp,являющейся верхней формулой самой нижней фигуры заключения предполагаемого вывода:


можно получить в результате применения фигуры заключения +, в том случае, если бы ранее в выводе мы вывели формулы q или р.

Например,

или

и предполагаемый вывод имел бы вид:

или .
Из двух указанных вариантов, по-видимому, предпочтительнее первый, в силу того, что формула р содержится в качестве подформулы допущения предполагаемого вывода. Мы хотим сказать, что формулу р можно было бы получить из формулы (pp)p применением фигуры заключения + при наличии формулы (pp):
.
Здесь формула pp не является допущением и следовательно, ее использование в выводе должно быть обосновано. При этом мы не должны выходить за рамки определения NJ-вывода. Вспомним еще раз основную идею NJ-вывода.

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

Заметим, что в определение NJ-вывода не входит ограничение на количество и вид допущений, главное - это то, чтобы конечная формула не зависела от них, а отбрасываемые допущения не изменяли ее структуры.

Это дает нам повод рассматривать формулу pp в виде конечной формулы некоторого вывода, "встроенного" в основной вывод:


Теперь переносим вывод, построенный над формулой pp, в основной вывод, и поскольку допущению (pp)p уже сопоставлено порядковое число +1, то допущению p мы сопоставим порядковое число +2.


Термин "встроенный вывод", хотя и употребляется в логической литературе, но, тем не менее, не является необходимым. Его использование носит скорее эвристический характер, поскольку часть вывода, оправдывающая использование в основном выводе той или иной формулы, строится в строгом соответствии с определением NJ-вывода.
***

Нам осталось рассмотреть примеры вывода формул, содержащих кванторы  и .

Пример 9. Пусть дана формула (xyFxy)(yxFxy). Действуем стандартным образом.

  1. Располагаем формулу в конце предполагаемого вывода:




  1. Формула имеет вид АВ, следовательно предыдущий шаг это:




  1. Вывод содержит одно допущение. Главным знаком формулы, взятой как допущение, является знак . Следовательно, предыдущий шаг - это применение фигуры заключения :

,
где в качестве F(a) берем формулу yFay, в качестве формулы С - формулу yxFxy.


4. Теперь рассмотрим незавершенную часть вывода:

.
5. Главным знаком формулы yxFxy является знак . Следовательно, предыдущий шаг - это применение фигуры заключения +, причем свободная переменная этого правила не должна входить ни в саму эту формулу, ни в допущение (yFay), от которого эта формула зависит. Пусть эта переменная будет обозначена символом b. Тогда рассматриваемая часть вывода будет иметь вид:


Главным знаком формулы xFxb является знак . Следовательно, предыдущий шаг - это применение фигуры заключения +, причем эта фигура заключения не содержит ограничений на переменные. Пусть такой переменной будет a.

.
6. Формулу Fab можно получить из формулы yFay применением фигуры заключения -.


7. Записываем вывод в целом:

***
Рассмотрим последний пример.

Пример 10. Пусть дана формула (xFx)(yFy) и необходимо построить ее вывод.

  1. Формула имеет вид АВ и следовательно, последний шаг в выводе - это:

.


  1. Главным знаком формулы yFy является знак , следовательно, предыдущий шаг это:




  1. Формула Fa - это результат применения фигуры заключения +:




  1. Итак, "пограничной" формулой данного вывода является формула Fa, и, следовательно, мы переходим ко второму этапу. Последующие шаги связаны с анализом списка допущений. Замечаем, что формулу "Л" можно получить с помощью фигуры заключения -, если верхними формулами этой фигуры будут формулы вида: А и А. У нас есть допущения xFx и Fa. Причем из формулы Fa применением фигуры заключения + можно получить формулу xFx, а именно:




а это и дает нам искомые формулы А и А


  1. Теперь основной вывод будет иметь следующий вид:



***
Подведем итоги. Поиск вывода в NJ-исчислении обладает рядом особенностей, которые определяются как структурой доказываемых формул, так и фигурами заключения самого NJ-исчисления. Мы установили, что процесс вывода распадается на два этапа:

  1. анализ структуры доказываемой формулы, т.е. нахождение антецедентов этой формулы (допущений вывода) и консеквента этой формулы ("пограничной" формулы вывода);

  2. выведение "пограничной" формулы из допущений.

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

На втором этапе мы

либо а) выводим "пограничную" формулу из уже обнаруженных допущений, в том случае, если этих допущений достаточно для выведения "пограничной" формулы (примеры 2, 3, 6, 7),

либо б) вводим дополнительные допущения, которые, участвуют в выводе, но не входят в качестве подформул в конечную формулу, в том случае, если уже известные допущения содержат знаки  и/или  (примеры 4, 5, 9, 10),

либо в) используем "встроенный" вывод, в том случае, если допущений, полученных согласно пунктам а) и б) недостаточно для выведения "пограничной" формулы (пример 8).

Наибольшую трудность при построении вывода представляет пункт в). Даже если формула доказуема в NJ-исчислении, то поиск ее вывода может оказаться весьма сложной процедурой, включающей в себя отыскание не одного, а многих "встроенных" выводов. Причем в этом случае мы не имеем строго формализуемых критериев завершенности поиска вывода. Например, если мы не можем найти вывод какой-либо формулы, то это не обязательно будет означать невыводимость данной формулы, это может означать и нашу неспособность найти вывод.

Таким образом, мы должны будем прибегать к некоторым косвенным оценкам выводимости той или иной формулы. Рассмотрим, например формулу (pq)p.

  1. Располагаем ее внизу предполагаемого вывода:


2.Предыдущий шаг:




  1. Непосредственно вывести формулу p из допущения pq мы не можем, так как у нас нет фигур заключения, дающих право на такие переходы. Дополнительные допущения мы также не можем ввести, поскольку допущение не содержит знаков , и . Попытка найти походящий встроенный вывод тоже не дает результатов, например:


Здесь мы взяли формулу p , чтобы получить формулу q, но как от q перейти к р остается неясным. Кроме того, нам не удастся обосновать использование формулы p. Далее мы могли бы попробовать придумать еще какую-либо формулу, например такую, что она вместе с первым допущением сразу позволит получить формулу р, а потом обосновать ее применение. Но такой формулой может быть формула (pq)p:

.
Однако, формула (pq)p именно та, которую мы должны доказать. Можно предпринять еще несколько попыток, но все они будут терпеть неудачу. На этом основании мы заключаем, что данная формула не выводима в нашем исчислении, и ясно, что это утверждение является скорее интуитивным, неопределенным и не поддается в рамках NJ-исчисления строгому процедурному описанию. Тем не менее, завершая описание доказательств в NJ-исчислении, попробуем сформулировать процедуру построения NJ-вывода для заданной формулы.

***
Процедура построения NJ-вывода заданной формулы.

  1. Располагаем правильно построенную формулу внизу предполагаемого вывода.

  2. Обратным применением NJ-фигур заключения восстанавливаем предполагаемый вывод в точности до получения "пограничной" формулы (косеквента доказываемой формулы).

Примечание: а) во втором параграфе мы уже говорили об особом месте, которое занимают фигуры заключения для отрицания. В частности, конечную формулу вывода, главным знаком которой является "отрицание", мы будем рассматривать одновременно и как "пограничную" формулу, в силу того, что она является и консеквентом нулькратной импликации, и содержит допущение в качестве подформулы; б) Конечные формулы вывода могут иметь в качестве главных знаков и знаки, отличные от импликации и отрицания. Тогда это будут знаки , &,  и . И они будут вводиться в конечную формулу только с помощью фигур заключения: +, &+, + и +, Это означает, что такие конечные формулы будут содержать подформулы, для которых будет применима эта процедура.

  1. Если полученные допущения содержат в качестве главного знака либо знак , либо , то к каждому из таких допущений, добавляем допущения, которые обычно сопоставляются фигурам заключения и .

  2. Из полученного списка допущений выводим "пограничную" формулу и восстанавливаем вывод в целом.

  3. Если указанного списка допущений недостаточно для выведения "пограничной" формулы, то ищем "встроенный" вывод и, в случае успеха, восстанавливаем вывод в целом.

  4. Если в результате применения пунктов 2-5 попытка построить вывод заданной формулы терпит неудачу, то останавливаем процедуру.


На этом мы заканчиваем рассмотрение доказательств в NJ-исчислении и переходим к исчислению NK.

***
1   2   3   4   5

Похожие:

Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconКлассическое определение вероятности. Комбинаторные методы решения задач
Цель: выработать умение решать задачи на определение классической вероятности с использованием основных формул комбинаторики
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconПриме Например, представим систему, которая состоит из трех подсистем. Соответственно, и требования могут быть разбиты на три части. Это можно представить в виде дерева следующим образом
Извлекаемые из документации требования представляются в виде дерева требований. Каждый узел-родитель в этом дереве является обобщением,...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon2001 Дифференциальное исчисление функции одной переменной. Производная функции, ее геометрический и физический смысл. Определение
Определение. Производной функции f(x) в точке х = х0 называется предел отношения приращения функции в этой точке к приращению аргумента,...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconПринципиальная схема сеточного метода решения детерминированного эквивалента стохастической задачи управления портфелем финансовых инструментов
Х переменных в динамике. Ключевая идея состоит в генерировании множества сценариев реализации случайных параметров в виде дерева...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconОпределение и свойства предела последовательности. Определение
Определение: задать числовую последовательность – это значит сопоставить каждому номеру действительное число
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconРешение задач на вывод формул органических веществ. Алгоритм решения задач на вывод формул органических веществ
Обозначить формулу вещества с помощью индексов Х,у,z и т д по числу элементов в молекуле. Если продуктами горения являются со2 и...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconУрок по теме «Функция квадратного корня»
В последствии появилось определение функции, данное Эйлером 1751 год, затем — у Лакруа в 1806 году — уже практически в современном...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconА. Определение: множество неограниченно. Определение: последовательность удовлетворяет критерию Коши. Определение: последовательность не удовлетворяет критерию Коши. Определение точной верхней грани. Определение точной нижней грани

Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon«Определение степени с целым показателем»
Образовательная: дать определение дроби с целым показателем, научить представлять степень с целым отрицательным показателем в виде...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon§ Определение доказуемой (выводимой) формулы
Следующим этапом в построении исчисления высказываний является выделение класса доказуемых (выводимых) формул
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org