Extensional Reasoning

Relational databases have had great industrial success in computer science, their power evidenced by theoretical analysis and widespread adoption. Often, automated theorem provers do not take advantage of database query engines and therefore do not routinely leverage that source of power. Extensional Reasoning is a novel approach to automated theorem proving where the system automatically translates a logical entailment query into a query about a database system so that the answers to the two queries are the same. This paper discusses the framework for Extensional Reasoning, describes algorithms that enable a theorem prover to leverage the power of the database in the case of axiomatically complete theories, and discusses theory resolution for handling incomplete theories.

• Type: Conference
• Year: 2007
• Where: SARA
• Authors: Timothy L. Hinrichs
• Keywords: Artificial Intelligence, Automated Theorem Provers, Extensional Reasoning, SARA 2007, Theorem Prover