Основы построения и функционирования интеллектуальных информационных систем. Былкин В.Д - 18 стр.

UptoLike

ВУЗ: 

ПГУ | Пенза

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

Рубрика: 

18
Подформулой называется любая часть формулы, которая сама является формулой.
3. Выделено некоторое множество формул, называемых аксиомами (в записях опущен знак
конъюнкции "&").
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
Каждая аксиома считается выводимой в ИВ.
4. Задано конечное множество отношений между формулами, называемыми правилами
вывода. В ИВ определено два правила вывода: а) правило заключения (модус поненс); б) правило
подстановки. Правило заключения формулируется следующим образом: если A В и А
выводимы в ИВ, то В - выводимая в ИВ Формула. Кратко это записывается так:
Дадим формулировку правила подстановки. Пусть А - формула, содержащая в качестве
подформулы формулу x . Тогда, если А выводимая формула, то, заменив x всюду, где она входит,
произвольной формулой В, получим выводимую формулу. Кратко это записывается так:
Доказательство формулы А в ИВ называется конечная последовательность формул В
1
, ... ,
Bn , где а) Bn А; б) Bi (i = 1, ... , n) есть любая аксиома, либо формула, полученная из
предыдущих формул по одному из правил вывода. Запись |— А означает, что А доказуема
(выводима) в ИВ, при этом формула А является тав-
)( xyx
))()(())(( zxyxzyx
xxy
yxy
)( xyyx
yxx v
yxy v
))v()(()( zyxzyzx
xx
xx
B
ABA ,
)(AS
A
B
x
         Подформулой называется любая часть формулы, которая сама является формулой.
         3. Выделено некоторое множество формул, называемых аксиомами (в записях опущен знак
конъюнкции "&").

1. x ( y x)
2. ( x ( y z ))            (( x    y)     (x      z ))
3. xy x
4. xy y
5. x ( y xy)
6. x xvy
7. y xvy
8. ( x z ) (( y            z)     ( xvy    z ))

9. ( x       y)       (y   x)

10.      x        x
11.       x x
         Каждая аксиома считается выводимой в ИВ.
         4. Задано конечное множество отношений между формулами, называемыми правилами
вывода. В ИВ определено два правила вывода: а) правило заключения (модус поненс); б) правило
подстановки. Правило заключения формулируется следующим образом: если A                      В и А
выводимы в ИВ, то В - выводимая в ИВ Формула. Кратко это записывается так:

                                              B, A            A
                                             B
         Дадим формулировку правила подстановки. Пусть А - формула, содержащая в качестве
подформулы формулу x . Тогда, если А выводимая формула, то, заменив x всюду, где она входит,
произвольной формулой В, получим выводимую формулу. Кратко это записывается так:

                                                      A
                                                  S xB ( A)
         Доказательство формулы А в ИВ называется конечная последовательность формул В1 , ... ,
Bn , где а) Bn             А; б) Bi (i = 1, ... , n) есть любая аксиома, либо формула, полученная из
предыдущих формул по одному из правил вывода. Запись |— А означает, что А доказуема
(выводима) в ИВ, при этом формула А является тав-




                                                                  18

Страницы