Softie - A Gentle Approach to Semantic Guidance in First-Order Theorem Proving
Mr. Arnold Binas (Texas A&M University, USA)
CSL SEMINAR SERIESDATE: 2003-08-19
TIME: 16:00:00 - 17:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
This will be a double act talk between Arnold Binas and John Slaney.
Various versions of the first-order theorem prover SCOTT have
been developed over the past decade to employ the concept of
semantic guidance for improving the underlying system OTTER.
In this talk, we review the previous versions of SCOTT and introduce
the latest attempt to speed up OTTER's proof search: Softie. While SCOTT
consults the constraint solver FINDER to gain information about the problem
to be solved, Softie employs the new SFINDER, which is capable of handling
soft constraints. Various parameters determine Softie's behaviour
with related experiments and preliminary findings being presented in
this talk. While much remains to be done, this early work shows some
mixed, yet encouraging results.
BIO:
Arnold Binas is currently an undergraduate student in the Department
of Computer Science at Texas A&M University in College Station.
He is a NICTA vacation scholar working on a project on semantic guidance
for first-order theorem proving under the supervision of John Slaney.
