#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.
- Используйте эти команды в качестве вступительных слов к вашим примерам.
В зависимости от вашей логики, вы также можете попытаться выразить их, используя предопределенные логики, такие как массивы, вместо обычной логики первого порядка.