| Relational databases have had great industrial success in computer science; however, most automated theorem provers today do not take advantage of database query engines and therefore do not routinely leverage that source of power. Extensional Reasoning is an approach to automated deduction where the system automatically translates an entailment query expressed in classical logic into a query about a database system so that the answers to the two queries are the same. To prove the theorem, the system then evaluates the database query using an off-the-shelf database.; Extensional Reasoning was developed because many problems can be solved efficiently using a database but are naturally expressed using classical logic. In some cases, database query engines solve the database version of the query orders of magnitude faster than traditional theorem proving techniques solve the classical version. Extensional Reasoning helps us build systems that allow a non-expert to write problems down naturally, convert those problems to efficient representations automatically, and solve those problems using industrial-strength systems.; Conceptually, algorithms for performing Extensional Reasoning can be broken into two classes: those for complete theories and those for incomplete theories. A complete theory, one that can answer all the questions in its vocabulary, corresponds naturally to a relational database. Algorithms for this class of theories must recognize the theory is complete and then construct the appropriate database system. In the context of a logic with a finite domain, I present incomplete but low-order polynomial-time algorithms for performing these tasks. An incomplete theory, one for which there is some question in the vocabulary that cannot be answered, does not correspond naturally to a database system, and so the algorithms for performing Extensional Reasoning are more complex. In this case my approach is to construct a new, complete theory that captures the information pertinent to the original problem---a novel form of theory-completion. I present algorithms for performing this type of theory-completion in the same finite logic. |
