Как добавить новую логику через Z3 или SMT-Lib? - PullRequest
Новая
       21

Как добавить новую логику через Z3 или SMT-Lib?

0 голосов
/ 12 марта 2019

У меня есть теоретическая часть, где я описываю новую логику и хочу ее реализовать.Но я не хочу делать все с нуля.

Я вижу большой потенциал в SMT-Lib / Z3, так как я могу реализовать свою логику с помощью этих инструментов?

И после реализации я собираюсь запустить несколько примеров, основанных на моей логике.

1 Ответ

0 голосов
/ 22 марта 2019
  • Аксиоматизируйте вашу логику в отсортированной логике первого порядка.
  • Объявите логические сортировки и символы и добавьте аксиомы в формате SMT-LIB.
  • Используйте эти команды в качестве преамбул к вашим примерам.

В зависимости от вашей логики вы можете также попытаться выразить их с помощью заранее определенных логик, таких как массивы, вместо простой первойлогика.

...