Представяне на правила за извод в 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, които имате, са абсолютно еднакви, това умишлено ли е?) Но по същество правилата за извод са импликации, така че да мислим за тях от гледна точка на предложения и импликации между тях би било добре.

Освен това вашите правила вероятно ще имат структура на Horn (както в клаузите на Horn, както се намират в Prolog, вижте тук: 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 от програма с това. Но това трябва да е толкова просто, колкото преминаване през AST и прилагане на правилата в z3 към дървото, прав ли съм? - person lilott8; 11.07.2017
comment
Това звучи много типично: изграждате AST и го обхождате символично, за да изплюете ограниченията. Изводът за тип, например, може да бъде изведен в тези условия, което звучи много подобно на вашето приложение. Вижте тук за интересно приложение на тази идея: microsoft.com/en-us/research/wp-content/uploads/2010/12/ - person alias; 11.07.2017