λProlog отклоняет гипотетические логические запросы?

Question

Я подозреваю, что teyjus, основная реализация λProlog, может быть немного заброшенным, но λProlog — это увлекательный Пролог, который должен позволить вам использовать логику более высокого порядка, гипотетические рассуждения и другие вещи, поэтому я пытаюсь используй это.

Файл "example.sig":

      sig example.

kind person, language type.

type hans person.
type german, french, italian language.

type grade person -> o.
type take person -> language -> o.

Файл "пример.мод":

      module example.

(grade P) :- (take P german), (take P french).
(grade P) :- (take P german), (take P italian).

take hans french.

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

      [example] ?- take X Y.

The answer substitution:
Y = french
X = hans

More solutions (y/n)? y

no (more) solutions

[example] ?- grade X.

no (more) solutions

[example] ?- (take hans german) => (grade hans).
(1,19) : Error : Symbol => is not permitted within terms

Я ожидал "да" в конце. Что я делаю не так?

Answer 1

Текущая версия Teyjus не позволяет вводить импликации в запросах непосредственно на верхний уровень. В книге Гопалана Надатура и меня (Programming with Higher-Order Logic) эта проблема и обходной путь упоминаются в Приложении (см. отрывок ниже).

A.4.2 Отклонения от языка, принятого в этой книге (стр. 287)

[...]

Тейюс не разрешает использовать импликации в целях высшего уровня. Эта характеристика может измениться в будущем, когда модель компиляции будет расширена и для этих целей, но на данный момент это означает, что некоторые примеры, представленные, например, в Разделе 3.2, не могут быть запущены непосредственно с помощью этой системы. Обратите внимание, что импликации запрещены только в целях верхнего уровня: их можно свободно использовать в целях, которые появляются в основной части пунктов программы. Таким образом, это ограничение можно преодолеть, сначала создав подходящее предложение программы, а затем используя его для постановки желаемого запроса. Например, вместо постановки запроса

      ?- p a => p b => p X.

можно создать пункт

      test X :- p a => p b => p X.

а затем используйте запрос

      ?- test X.

Answer 2

Расширьте «example.sig»:

      type whatif language -> o.

Расширьте «example.mod»:

      (whatif Q) :- ((take hans Q) => (grade hans)).

И тогда это работает:

Похоже, что λProlog отложен, я поднял вопрос №122 .
Или есть какая-то фундаментальная проблема, с которой он не работает,
например, проблемы с типизацией или оптимизация компилятора?

PS: я жил опасно и скачал tjsim.exe и т. д. отсюда:
http://www.eecs.ucf.edu/~leavens/Windows/usr-local-bin/