Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

AIC Seminar Series

Extensional Reasoning: Datalog-based Deduction

Tim HinrichsStanford University

Notice:  hosted by Richard Waldinger

Date:  Thursday, September 6th 2007 at 4:00pm

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 non-expert to write problems down naturally, convert the problem to an efficient representation automatically, and solve that problem using industrial-strength 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 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 our approach constructs a new, complete theory that captures the information pertinent to the original problem—a novel form of theory-completion. We present algorithms for performing this type of theory-completion in the same finite logic.

   Bio for Tim Hinrichs

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 industrial-strength database algorithms.

   Note for Visitors to SRI

Please arrive at least 10 minutes early as you will need to sign in by following instructions by the lobby phone at Building E (or call Wilma Lenz at 650 859 4904, or Eunice Tseng at 650 859 2799). 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 Building E entrance signage.

SRI International
©2018 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy