AIC Seminar Series
High Performance Lean Theorem Proving
|Jens Otten||University of Potsdam, Germany||[Home Page]|
Notice: Hosted by Richard Waldinger. Note the non-usual weekday (Tuesday)
Date: Tuesday, September 21st 2010 at 4:00pm
Location: EJ228 (SRI E Building). Slides via WebEx from 3:45pm on, sound at 1-888-355-1249, 749045 (Directions)
leanCoP is an automated theorem prover for classical first-order logic. It is implemented in Prolog and the source code of the core proof search algorithm is only a few lines long. Despite it's compact size, leanCoP is currently one of the fastest theorem provers that output a proof.
We introduce the underlying basic calculus, describe a few essential techniques to prune the search space, and present details of the actual implementation. Furthermore, we explain how leanCoP can be extended to deal with intuitionistic logic as well as with linear integer arithmetic.
See leanCoP's home page at www.leancop.de for more details.
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 Vicenta at Lopez at 650 859 5750). 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.
©2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493