Campus Event Calendar

Event Entry

What and Who

Higer-order Equational Logic

Prof. Dr. Gert Smolka
AG 1, AG 2, AG 3, AG 4, AG 5  
AG Audience

Date, Time and Location

Thursday, 23 June 2005
-- Not specified --


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.


--email hidden

Bahareh Kadkhodazadeh, 06/21/2005 03:09 PM
Bahareh Kadkhodazadeh, 04/07/2005 03:54 PM -- Created document.