Campus Event Calendar
Event Entry
What and Who
Integrating Isabelle with Automatic Theorem
Lawrence C. Paulson
University of Cambridge
Informatikkolloquium
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 30 June 2005
16:00
-- Not specified --
45
HS 001
Saarbrücken
Abstract
Provers: Status and ProspectsCombining interactive and
automatic theorem provers is anobvious idea, but it contains
surprising complexities. Theinteractive user can derive little
benefit from merelyquerying an automatic prover: to be useful, the
integrationmust be deep, which complicates the implementation.
Thespeaker will describe the project, ongoing at Cambridge, tointegrate
Isabelle with saturation- based theorem provers,primarily SPASS. He
will outline the potential benefits(including the less obvious
ones). He will also describe theproblems that have been encountered,
including irrelevancefiltering, higher-order reasoning and
presenting lengthyproofs to users. Some of these issues are avenues for
futureresearch.
automatic theorem provers is anobvious idea, but it contains
surprising complexities. Theinteractive user can derive little
benefit from merelyquerying an automatic prover: to be useful, the
integrationmust be deep, which complicates the implementation.
Thespeaker will describe the project, ongoing at Cambridge, tointegrate
Isabelle with saturation- based theorem provers,primarily SPASS. He
will outline the potential benefits(including the less obvious
ones). He will also describe theproblems that have been encountered,
including irrelevancefiltering, higher-order reasoning and
presenting lengthyproofs to users. Some of these issues are avenues for
futureresearch.
Contact
--email hidden
passcode not visible
logged in users only
Bahareh Kadkhodazadeh, 06/21/2005 15:12 -- Created document.