Extensional Reasoning: Datalogbased Deduction
Tim Hinrichs  Stanford University 
Notice: hosted by Richard Waldinger
Date: 20070906 at 16:00
Location: EJ228 (SRI E building) (Directions)

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, as far as we know, a novel 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. 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 to build systems that allow a nonexpert to write problems down naturally, convert the problem to an efficient representation automatically, and solve that problem using industrialstrength systems. Algorithms for Extensional Reasoning can conceptually 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 deductive 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, we present incomplete but loworder polynomialtime 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 our approach constructs a new, complete theory that captures the information pertinent to the original problemÂ—a novel form of theorycompletion. We present algorithms for performing this type of theorycompletion in the same finite logic. 

Hinrichs is a Ph.D. candidate at Stanford University studying computational logic: the representation and processing of knowledge in a logical form. Currently he is interested in the relationships between some of the most successful applications of logic in computer science: theorem proving, deductive databases, logic programming, constraint satisfaction, boolean satisfiability, and model checking. His thesis, Extensional Reasoning, automatically transforms theorem proving problems in a finite logic into deductive database problems, implicitly proving theorems using industrialstrength database algorithms. 

Please arrive at least 10 minutes early as you will need to sign in by following instructions by the lobby phone at Building E. SRI is located at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the parking lots off Fourth Street. Detailed directions to SRI, as well as maps, are available from the Visiting AIC web page. There are two entrances to SRI International located on Ravenswood Ave. Please check the Builing E entrance signage.
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 940253493
SRI International is an independent, nonprofit corporation. Privacy policy 