Reformulation for Extensional Reasoning

Relational databases have had great industrial success in computer science. The power of the paradigm is made clear both by its widespread adoption and by theoretical analysis. Today, automated theorem provers are not able to take advantage of database query engines and therefore do not routinely leverage that source of power. Extensional Reasoning (ER) 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 such that the entailment query can be answered by answering the database query. The techniques developed for ER to date are applicable only when the logical theory is axiomatically complete. This paper discusses techniques for reformulating an incomplete theory into a complete theory so that Extensional Reasoning techniques can be applied.

• Type: Conference
• Year: 2007
• Where: SARA
• Authors: Timothy L. Hinrichs, Michael R. Genesereth
• Keywords: Artificial Intelligence, Database Query, Entailment Query, Extensional Reasoning, SARA 2007