From pa01@gtps.math.cmu.edu Mon Nov  3 17:10:50 2008
Date: Mon, 03 Nov 2008 17:10:49 -0500
From: Peter Andrews <pa01@gtps.math.cmu.edu>
To: kk3n@andrew.cmu.edu, ws15@andrew.cmu.edu, Steven Awodey <awodey@cmu.edu>, Frank Pfenning <fp@cs.cmu.edu>, Richard Statman <rs31@andrew.cmu.edu>, Edmund Clarke <emc@cs.cmu.edu>
Subject: Benzmuller talk 


	Here is the preliminary announcement. It should be sent to 
the complete PAL mailing list soon.

		Pure and Applied Logic Colloquium

Speaker: Christoph Benzmuller
	 On leave from Saarland University
Date: Wednesday, November 19, at 4:30 p.m.
Place: Baker Hall 237B

Title: Automating Access Control Logics and Multimodal Logics
       in the Automatic Higher-Order Theorem Prover LEO-II

Abstract:
   LEO-II is a standalone, resolution-based higher-order theorem 
   prover designed for effective cooperation with specialist 
   provers for natural fragments of higher-order logic. 
   At present LEO-II can cooperate with the first-order automated 
   theorem provers E, SPASS, and Vampire. LEO-II is implemented in
   Objective Caml and its problem representation language is the new
   TPTP THF language.
   We demonstrate that problems in normal multimodal logic and 
   access control logics can be elegantly encoded simple type theory 
   and automated in LEO-II.