Computational Logic Seminar

Date and Time: October 21, 2004 @ 1:30pm

Place: ASB 9705

Speaker:

Geoff Sutcliffe (and the ARTists group)

Department of Computer Science, University of Miami

Title:

Automated Theorem Proving for Hard Theorems in Rich Theories

Abstract:

Automated Theorem Proving (ATP) is concerned with the development and use of
systems that automate sound reasoning: the derivation of conclusions that follow
inevitably from facts. A Rich Theory is one whose axioms (expressed in 1st order
logic) contain a large number of predicates and functors, and whose theorems
are often provable from a subset of the axioms. While theorems in rich theories
are often hard for an individual ATP system to prove, the richness provides
sources of information and opportunities to use high level ATP techniques intelligent
ways. This seminar outlines several interlinked projects whose common goal is
to prove hard theorems in rich theories, using ATP systems within higher level
control systems. The projects include analysis and selection of axioms for proving
a given conjecture, the automatic generation and use of lemmas, cooperative
competition between ATP systems, and semantic verification of proofs.

http://www.cs.sfu.ca/~cl