Представление правил вывода в z3

Я читал и прорабатывал несколько частей документации, но до сих пор не понимаю, как представить мои правила вывода в z3.

Допустим, у меня есть следующие 2 правила вывода:

игровые правила вывода для вопроса

Так ли просто, что мои правила z3 будут такими:

a. (a ^ b) => c
b. (a ^ b) => c

Или, что я считаю более правильным, мне придется объявлять типы данных (записи, скаляры и т.д.).

Оттуда реализация Java кажется довольно простой из чтения документации.

Это просто первоначальный перевод от правил вывода системы типов к пропозициональной логике, который меня подвешивает.

Я думаю, что мне не хватает какой-то связи между моими правилами вывода (a и b) и их представлением в z3; и поскольку я продолжаю читать документацию, все еще остается неясным, как реализовать эти правила.


java z3
person lilott8    schedule 10.07.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Z3 был бы прекрасным выбором для этой задачи, хотя очень сложно точно понять, в чем заключается ваш вопрос. (Точки a и b у вас точно такие же, было ли это преднамеренно?) Но, по сути, правила вывода являются импликациями, поэтому думать о них с точки зрения предложений и импликаций между ними было бы вполне нормально.

Кроме того, ваши правила, вероятно, будут иметь структуру Хорна (как в предложениях Хорна, которые можно найти в Прологе, см. здесь: https://en.wikipedia.org/wiki/Horn_clause), а Z3 имеет механизм регистрации данных, который может сделать кодирование таких проблем еще проще.

См. здесь очень хорошее введение: http://rise4fun.com/z3/tutorialcontent/fixedpoints который, я думаю, можно относительно легко адаптировать к вашему варианту использования.

person alias    schedule 11.07.2017
comment
Это было сделано намеренно. Все мои правила вывода для моего реального языка следуют очень похожей схеме — это простой язык. Я мог бы так же легко добавить время или если: if Bool then {statement_1} else {statement_2}. И даже это правило вывода будет похоже на «а» и «б». while фактически совпадает с if. Я как раз мучился с преобразованием вывода в пропозиции и очень боялся, что все они будут выглядеть почти одинаково. - person lilott8; 11.07.2017
comment
И, конечно же, следующая остановка — манипулировать AST из программы с помощью this. Но это должно быть так же просто, как пройти через AST и применить правила в z3 к дереву, я прав? - person lilott8; 11.07.2017
comment
Звучит очень типично: вы строите AST и символически проходите его, чтобы выявить ограничения. Вывод типа, например, может быть выражен в этих терминах, что очень похоже на ваше приложение. См. здесь интересное применение этой идеи: microsoft.com/en-us/research/wp-content/uploads/2010/12/ - person alias; 11.07.2017