Combining Finite Combination Properties: Finite Models and Busy Beavers

FRONTIERS OF COMBINING SYSTEMS, FROCOS 2023(2023)

引用 0|浏览25
暂无评分
摘要
This work is a part of an ongoing effort to understand the relationships between properties used in theory combination. We here focus on including two properties that are related to shiny theories: the finite model property and stable finiteness. For any combination of properties, we consider the question of whether there exists a theory that exhibits it. When there is, we provide an example with the simplest possible signature. One particular class of interest includes theories with the finite model property that are not finitely witnessable. To construct such theories, we utilize the Busy Beaver function.
更多
查看译文
关键词
satisfiability modulo theories,theory combination,theory politeness,theory shininess
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要