– Программа, написанная на языке C++ (-std=c++17), которой можно передавать утверждения и запросы, представленные в логике первого порядка. Для выполнения запросов используется метод резолюции.
- Википедия
- Resolution Theorem Proving (First Order Logic - Cornell CS)
- Resolution (Technische Universität München)
- Лиз – мать Чарли.
- Чарли – отец Билли
- Если x – мать y, тогда x – один из родителей y
- Если x – отец y, тогда x – один из родителей y
- Если x – родитель y, тогда x – предок y
- Если x – родитель y и y – предок z, тогда x – тоже предок z.
Эти высказывания можно представить в логике первого порядка следующим образом:
Mother(Liz,Charley)
Father(Charley,Billy)
∀x,y (Mother(x,y) → Parent(x,y))
∀x,y (Father(x,y) → Parent(x,y))
∀x,y (Parent(x,y) → Ancestor(x,y))
∀x,y,z ((Parent(x,y) ∧ Ancestor(y,z)) → Ancestor(x,z))
Затем из выражений удаляются кванторы, после чего первые можно передавать программе:
!- Mother(Liz,Charley)
!- Father(Charley,Billy)
!- Mother(x,y) => Parent(x, y)
!- Father(x,y) => Parent(x, y)
!- Parent(x,y) => Ancestor(x, y)
!- Parent(x,y) & Ancestor(y,z) => Ancestor(x,z)
Передадим интересующие нас запросы:
?- Ancestor(Liz,Billy)
?- Ancestor(Liz,Bob)
И получим вывод:
Y:\FOLEngine\Debug>FOLEngine.exe ..\test1.txt
Ancestor(Liz,Billy) :: YES
Ancestor(Liz,Bob) :: NO
!- Cat(x) => Animal(x)
!- Dog(x) => Animal(x)
!- Cat(Tuna)
!- Dog(D)
!- Owns(Jack,D)
!- Kills(Jade,Tuna)
!- Animal(y) & Owns(x,y) => AnimalLover(x)
!- Animal(y) & Owns(x,y) => HasOwner(y)
!- ~(AnimalLover(x) & Animal(y) & Kills(x,y))
# Комментарий
?- AnimalLover(Jade)
?- HasOwner(D)
Ответ:
Y:\FOLEngine\Debug>FOLEngine.exe ..\test2.txt
AnimalLover(Jade) :: NO
HasOwner(D) :: YES