Математическая логика и теория алгоритмов. Сергиевская И.М. - 18 стр.

UptoLike

ВУЗ: 

ПГУТИ | Самара

Составители: 

Рубрика: 

23
4.
C
B
→ . MP 3,1.
5.
C
. MP 2,4.
3)
По теореме, обратной теореме дедукции, ├
(
)
(
)
(
)()
CABCBA →→→→→
равносильно
()
ABCBA ,,→→ ├
C
.
1.
()
CBA →→ – гипотеза.
2.
B
– гипотеза.
3.
A
– гипотеза.
4.
C
B
→ . MP 2,1.
5.
C
. MP 2,4.
3. Построить вывод формулы.
1)
()
(
)()
(
)()
CACBABA →→→→→→ .
2)
()
))()(( CACBBA →→→→→
.
3)
→→ )(
B
A
→→ )((
C
B
→→ )(( D
C
)))( D
A
→ .
4)
)(
B
A
A
→→¬ .
5)
A
A
→¬¬ .
6)
A
A
¬¬→ .
7)
()
BABA →→¬¬→ )(
.
8)
()
BABA →→→¬¬ )(.
9)
()
ABBA ¬→¬→→ )( .
10)
))((
B
A
B
A
→¬→¬→ .
11)
()( )()
BABBA →→¬→→ .
12)
()()
AABA →→→ .
В
Ответы и указания.
В
Содержание.
Глава 4. Метод резолюций в логике высказываний.
Метод резолюций – это метод автоматического доказательства теорем –
основы логического программирования. Это алгоритм, проверяющий отношение
выводимости
Γ
├
A
. В общем случае алгоритм автоматического доказательства
теорем не существует, но для формальных теорий с несложной структурой (таких
как исчисление высказываний, исчисление предикатов с одним одноместным
предикатом) подобные алгоритмы известны.
Вообще говоря, в построенном в главе 3 исчислении высказываний (благодаря
полноте исчисления) проверка выводимости формулы состоит в проверке того, 
   4. B → C .                                   MP 3,1.
   5. C .                                       MP 2,4.
3) По теореме, обратной теореме дедукции, ├ ( A → (B → C )) → (B → ( A → C ))
   равносильно A → (B → C ), B, A ├C .
   1. A → (B → C ) – гипотеза.
   2. B – гипотеза.
   3. A – гипотеза.
   4. B → C .                                   MP 2,1.
   5. C .                                       MP 2,4.

       3. Построить вывод формулы.
1) ( A → B ) → (( A → (B → C )) → ( A → C )) .
2) ( A → B ) → (( B → C ) → ( A → C )) .
3) ( A → B ) → (( B → C ) → ((C → D) → ( A → D))) .
4) ¬A → ( A → B) .
5) ¬¬A → A .
6) A → ¬¬A .
7) ( A → ¬¬B) → ( A → B ).
8) (¬¬A → B) → ( A → B ) .
9) ( A → B) → (¬B → ¬A) .
10)      A → (¬B → ¬( A → B)) .
11)     ( A → B ) → ((¬B → A) → B ) .
12)     (( A → B ) → A) → A .
В Ответы и указания.
В Содержание.




Глава 4. Метод резолюций в логике высказываний.

     Метод резолюций – это метод автоматического доказательства теорем –
основы логического программирования. Это алгоритм, проверяющий отношение
выводимости Γ ├ A . В общем случае алгоритм автоматического доказательства
теорем не существует, но для формальных теорий с несложной структурой (таких
как исчисление высказываний, исчисление предикатов с одним одноместным
предикатом) подобные алгоритмы известны.
     Вообще говоря, в построенном в главе 3 исчислении высказываний (благодаря
полноте исчисления) проверка выводимости формулы состоит в проверке того,


                                          23

Страницы