A Fresh Look at the Given Clause Algorithm
John Slaney (CSL/NICTA)
CSL SEMINAR SERIESDATE: 2005-12-01
TIME: 16:00:00 - 17:00:00
LOCATION: Video Conference Room, A207, RSISE
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
The given clause algorithm is the basis of most contemporary high performance theorem provers, and has been so for some decades. Surprisingly, in all that time nobody seems to have looked carefully at what actually happens during bottom-up proof searches. The present talk reports some early findings from a project on visualisation of automated reasoning. It does not reach a simple conclusion but rather demonstrates the complexity of the processes hidden behind the usual runtime statistics such as the number of loop iterations or the number of clauses generated.
This work is part of the HULC project involving the Logic and
Computation Program and the Interfaces, Machines and Graphic
Environments (IMAGEN) Program. The talk was given at the seminar
"Deduction and Applications" at Schloss Dagstuhl last month.
BIO:
