Campus Event Calendar
Event Entry
What and Who
Higer-order Equational Logic
Prof. Dr. Gert Smolka
Ringvorlesung
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, 23 June 2005
13:00
-- Not specified --
45
016
Saarbrücken
Abstract
Higher Order Logic (HOL) is an expressive language for
mathematical statements. It is employed by several
proof assistants used for formal verification.
We are investigating an axiomatization of HOL in a pure
equational logic S, which is a slight refinement of the
simply typed lambda calculus. This approach has the
advantage of modularity. The semantics and proof rules
of the logical constants (Boolean connectives,
quantifiers, identity) are no longer hard wired in, but
are obtained by equational axiomatization in the same
way this is done for ordinary constants. A second
advantage is the fact that all deduction is equational
deduction, which is a simple, familiar and powerful
form of mathematical reasoning. As it turns out,
treating quantifiers by equational deduction is
convenient for humans.
The talk will outline our approach and identify some
open problems. Familiarity with HOL is not required.
mathematical statements. It is employed by several
proof assistants used for formal verification.
We are investigating an axiomatization of HOL in a pure
equational logic S, which is a slight refinement of the
simply typed lambda calculus. This approach has the
advantage of modularity. The semantics and proof rules
of the logical constants (Boolean connectives,
quantifiers, identity) are no longer hard wired in, but
are obtained by equational axiomatization in the same
way this is done for ordinary constants. A second
advantage is the fact that all deduction is equational
deduction, which is a simple, familiar and powerful
form of mathematical reasoning. As it turns out,
treating quantifiers by equational deduction is
convenient for humans.
The talk will outline our approach and identify some
open problems. Familiarity with HOL is not required.
Contact
--email hidden
passcode not visible
logged in users only
Bahareh Kadkhodazadeh, 06/21/2005 15:09
Bahareh Kadkhodazadeh, 04/07/2005 15:54 -- Created document.
Bahareh Kadkhodazadeh, 04/07/2005 15:54 -- Created document.