YAFOLL

Сегодня 15.01.15 хорошая дата чтобы зафиксировать на сайте рождение YAFOLL (Yet Another First Order Logic Language)! Кое уже отмечалось вчера в узком кругу G+.

И хотя ему (а точнее его процессору - Yp) ещё расти и совершенствоваться, но, как говорится, система задышала! А именно, энтузиаст (я одного знаю) может:

а) объявлять сорта, константы и частичные функции, а главное определять(!) константы и ч-функции.

Принимая во внимание что предикат является (обычно полной) функцией в истинностные значения мы имеем примерно FOL. Часть функций можно объявить первичными. Такие функции не имеют определений, но их можно задавать (см. дальше);

б) задавать состав (совокупность элементов) сортов,

в) задавать значение первичной функции на конкретных элементах сортов,

Таким образом есть возможность вести конечные алгебраические системы (и не только) - сокращённо КС (конечная система);

г) вычислять на КС значение замкнутого терма, в том числе предиката.

Последнее даёт возможность проверить является ли данная КС моделью данной совокупности аксиом.

Замечание о дате рождения. Предыдущая дата 14.01.14 была ошибкой длинных январских праздников.

Yp v.0.0 текущее (15.01.15) наполнение и запросы к нему

Исключительно ради праздника зафиксируем:

- DD - текущие, загруженные в ИС, объявления и определения.

- КС - текущую, загруженную в ИС, конечную систему.

- Q&A - парочку вопросов и ответов на них.

DD

Суть дела (кроме задания контекста работы со значениями истинности):

- сорт V (узлов) содержит два элемента: v1, v2.

- сорт A (стрелок) содержит 4 элемента: a1..a4.

- функции from, tov: из A в V.

Замечание. Назвать ф-ю to нельзя - это ключевое слово;-)

Ниже приведён результат работы спец-команды !1!, которая выдаёт не только DD, но и наполнение сортов. Yp оформляет протокол обработки порции предложений YAFOLL в виде xml-док.

<?xml version='1.0' encoding='UTF-8' ?>

<DT>

--DTS dump begin.

Declaration TV sort .

Declaration EQU_TV TV TV : TV prime .

Add infix "=" to EQU_TV .

Declaration NOT TV : TV prime .

Add infix "¬" to NOT .

Add infix "not" to NOT .

Declaration AND TV TV : TV prime .

Add infix "∧" to AND .

Add infix "and" to AND .

Declaration OR TV TV : TV prime .

Add infix "∨" to OR .

Add infix "or" to OR .

Declaration IMPLIES TV TV : TV .

Add infix "→" to IMPLIES .

Add infix "impl" to IMPLIES .

Definition IMPL_d IMPLIES ( x z ) : ( ( ¬ x ) ∨ z ) .

Definition IMPL_d IMPLIES ( x z ) : OR ( NOT ( x ) z ) .

Declaration EQUIV TV TV : TV .

Add infix "≡" to EQUIV .

Add infix "eqv" to EQUIV .

Definition EQV_d EQUIV ( x y ) : ( ( x → y ) ∧ ( y → x ) ) .

Definition EQV_d EQUIV ( x y ) : AND ( OR ( NOT ( x ) y ) OR ( NOT ( y ) x ) ) .

Declaration NEQ_TV TV TV : TV .

Add infix "≠" to NEQ_TV .

Add infix "neq" to NEQ_TV .

Definition NEQ_TV_d NEQ_TV ( x y ) : ( ¬ ( x = y ) ) .

Definition NEQ_TV_d NEQ_TV ( x y ) : NOT ( EQU_TV ( x y ) ) .

! True TV !

! False TV !

Declaration V sort .

Declaration EQU_V V V : TV prime .

Add infix "=" to EQU_V .

Declaration NEQ_V V V : TV .

Add infix "≠" to NEQ_V .

Add infix "neq" to NEQ_V .

Definition NEQ_V_d NEQ_V ( x y ) : ( ¬ ( x = y ) ) .

Definition NEQ_V_d NEQ_V ( x y ) : NOT ( EQU_V ( x y ) ) .

Declaration A sort .

Declaration EQU_A A A : TV prime .

Add infix "=" to EQU_A .

Declaration NEQ_A A A : TV .

Add infix "≠" to NEQ_A .

Add infix "neq" to NEQ_A .

Definition NEQ_A_d NEQ_A ( x y ) : ( ¬ ( x = y ) ) .

Definition NEQ_A_d NEQ_A ( x y ) : NOT ( EQU_A ( x y ) ) .

Declaration from A : V prime .

Declaration tov A : V prime .

! v1 V !

! v2 V !

! a1 A !

! a2 A !

Declaration source V : TV .

Definition source_d source ( x ) : ( ∀ e : A ( tov ( e ) ≠ x ) ) .

Definition source_d source ( x ) : ( ∀ e : A NOT ( EQU_V ( tov ( e ) x ) ) ) .

? ( ∀ e1 : A ( ∀ e2 : A ( ( tov ( e1 ) = from ( e2 ) ) → ( ∃ e3 : A ( ( from ( e3 ) = from ( e1 ) ) ∧ ( tov ( e3 ) = tov ( e2 ) ) ) ) ) ) ) ?

? ( ∀ e1 : A ( ∀ e2 : A OR ( NOT ( EQU_V ( tov ( e1 ) from ( e2 ) ) ) ( ∃ e3 : A AND ( EQU_V ( from ( e3 ) from ( e1 ) ) EQU_V ( tov ( e3 ) tov ( e2 ) ) ) ) ) ) ) ?

! a3 A !

! a4 A !

? ( ∀ e1 : A ( ∀ e2 : A ( ( tov ( e1 ) = from ( e2 ) ) → ( ∃ e3 : A ( ( from ( e3 ) = from ( e1 ) ) ∧ ( tov ( e3 ) = tov ( e2 ) ) ) ) ) ) ) ?

? ( ∀ e1 : A ( ∀ e2 : A OR ( NOT ( EQU_V ( tov ( e1 ) from ( e2 ) ) ) ( ∃ e3 : A AND ( EQU_V ( from ( e3 ) from ( e1 ) ) EQU_V ( tov ( e3 ) tov ( e2 ) ) ) ) ) ) ) ?

--DTS dump end.

</Yp1s>

</DT>

КС

Суть дела (за пределами контекста работы с истинностными значениями;-): термы назначены так, что стрела a1 идёт из v1 в v2, a2 - из v2 в v1, а a3, a4 - петли.

Ниже приведёна таблица парочек: терм и назначенное ему значение. Так терму from ( a1 ) назначено значение v1. Содержательно - стрела a1 исходит из узла v1.

Назначение значений одним термам даёт возможность вычислять значения других термов, а наполнение основ даёт возможность организовать пробег для кванторов:-)

" AND ( False False )";"False"

" AND ( False True )";"False"

" AND ( True False )";"False"

" AND ( True True )";"True"

" EQU_A ( a1 a1 )";"True"

" EQU_A ( a1 a2 )";"False"

" EQU_A ( a1 a3 )";"False"

" EQU_A ( a1 a4 )";"False"

" EQU_A ( a2 a1 )";"False"

" EQU_A ( a2 a2 )";"True"

" EQU_A ( a2 a3 )";"False"

" EQU_A ( a2 a4 )";"False"

" EQU_A ( a3 a1 )";"False"

" EQU_A ( a3 a2 )";"False"

" EQU_A ( a3 a3 )";"True"

" EQU_A ( a3 a4 )";"False"

" EQU_A ( a4 a1 )";"False"

" EQU_A ( a4 a2 )";"False"

" EQU_A ( a4 a3 )";"False"

" EQU_A ( a4 a4 )";"True"

" EQU_TV ( False False )";"True"

" EQU_TV ( False True )";"False"

" EQU_TV ( True False )";"False"

" EQU_TV ( True True )";"True"

" EQU_V ( v1 v1 )";"True"

" EQU_V ( v1 v2 )";"False"

" EQU_V ( v2 v1 )";"False"

" EQU_V ( v2 v2 )";"True"

" from ( a1 )";"v1"

" from ( a2 )";"v2"

" from ( a3 )";"v1"

" from ( a4 )";"v2"

" NOT ( False )";"True"

" NOT ( True )";"False"

" OR ( False False )";"False"

" OR ( False True )";"True"

" OR ( True False )";"True"

" OR ( True True )";"True"

" tov ( a1 )";"v2"

" tov ( a2 )";"v1"

" tov ( a3 )";"v1"

" tov ( a4 )";"v2"

Q&A

Вопрос-1. Являются ли функции from, tov полными?

Вход

?(∀e:A (∃v:V (from(e)=v)))?

?(∀e:A (∃v:V (tov (e)=v)))?

Выход

Полный протокол содержит много отладочной информации (см. прикреп акс_полн.Yp1.out.xml). Результат вычисления терма в xml-элементе answer:-)

Итак обе ф-и полные а значит мы имеем орграф;-)

Вопрос-2. Является ли орграф транзитивно замкнутым?

Вопрос

?(∀e1:A (∀e2:A ((tov(e1)=from(e2))→(∃e3:A ((from(e3)=from(e1)) ∧ (tov(e3)=tov(e2)))))))?

Ответ

Полный протокол содержит очень много отладочной информации (см. прикреп транз_зам.Yp1.out.xml). Результат вычисления терма в xml-элементе answer:-)

Ну вот - граф транзитивно замкнут:-)

ИДЕОЛОГИЯ YAFOLL как языка онтологистики

YAFOLL (сокращённо Y!L) задуман для онтологистики, исходя из следующих идей:

- язык онтологистики стоит сделать из FOL, пополнив его монгосортностью, строками и числами;

- В Y!L должна быть возможность давать определения,

- нужен язык задания моделей - по крайней мере алгебраических систем,

- модели будут конечными (рабочее название - конечная система(КС)).

Если на КС выполнены аксиомы предметной области, то мы имеем модель и вычисляя на ней те или иные формулы узнаём что-то интересное о той части реальности которую модель моделирует.

Page updated

Google Sites

Report abuse