带特设重载的 HOL 模型论保守扩张的机械化
计算机科学中的逻辑
2021-01-12 v1
摘要
新符号的定义仅仅是对逻辑框架中表达式的缩写，且不应因为新定义而成立任何关于先前已定义符号的新事实。在 Isabelle/HOL 中，可定义符号为类型和常量。后者可以是特设重载的，即对非重叠类型具有不同的定义。我们证明，独立于新定义的符号可在模型扩张中保持其解释。本工作修订了我们早先关于模型论保守扩张的概念，并推广了早先的模型构造。作为推论，我们得到了带特设重载的高阶逻辑（HOL）定义理论的一致性。我们的结果在 HOL4 定理证明器中得到了机械化。
引用
@article{arxiv.2101.03807,
title = {Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading},
author = {Arve Gengelbach and Johannes Åman Pohjola and Tjark Weber},
journal= {arXiv preprint arXiv:2101.03807},
year = {2021}
}
备注
In Proceedings LFMTP 2020, arXiv:2101.02835