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

#z3 #smt #z3py #lib

#z3 #smt #z3py #библиотека

Вопрос:

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

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

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

Комментарии:

1. Доказательства / верификация, использующие логику, более богатую, чем та, которую поддерживает SMT-LIB, обычно закодированы в SMT-LIB. Например, Viper ( viper.ethz.ch ) кодирует доказательства на основе логики разделения в SMT-LIB, что является очень сложным процессом. Это позволяет создать стек инструментов, в котором даже «более высокие» инструменты кодируют доказательства, используя еще более богатую логику, в Viper и, таким образом, в конечном итоге в SMT-LIB, как, например, здесь: описано link.springer.com/chapter/10.1007/978-3-319-89960-2_11 .

Ответ №1:

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

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