Extensional Reasoning
Extensional Reasoning
复制标题
外延推理
DOI：
10.1007/978-3-540-73580-9_35
复制
发表时间：
2007
影响因子：
20.6
通讯作者：
Timothy L. Hinrichs
中科院分区：
文献类型：
--
作者：
Timothy L. Hinrichs
关系数据库是形式逻辑在计算机科学中最成功的工业应用之一。范式的力量是显而易见的，因为它的广泛采用和理论分析。今天，自动化定理证明程序不能利用数据库系统，因此不能常规地利用这种能力。扩展推理是一种自动定理证明的方法，其中机器自动将逻辑蕴涵查询转换为数据库、一组视图定义和数据库查询，以便可以通过回答数据库查询来回答蕴涵查询。在某些情况下，这种方法比传统的定理证明技术产生了几个数量级的性能改进。
Relational databases are one of the most industrially successful applications of formal logic in computer science. The power of the paradigm is clear both because of its widespread adoption and because of theoretical analysis. Today, automated theorem provers are not able to take advantage of database systems and therefore do not routinely leverage that source of power. Extensional Reasoning is an approach to automated theorem proving where the machine automatically translates a logical entailment query into a database, a set of view definitions, and a database query so that the entailment query can be answered by answering the database query. In some cases this approach produces several orders of magnitude performance improvement over traditional theorem proving techniques.