UMass Lowell
Computer Science Colloquium 
Announcement
 
 
Speaker: Professor Ray Gumb
 Dept of Computer Science, UMass Lowell. Email: gumb@cs.uml.edu
Date: December 5, 2001 
Time: 3:30pm--4:30pm
Place: Olsen 311 (The Media Lab)
 Refreshments are served at 3:00pm



 
  
 
 
  
  
 


 

Logic for Specifying and Verifying Programs, Part I 
 
The logic of partial terms (LPT) is a variant of the negative
free logic introduced by Rolf Schock thirty years ago. Similar 
logics are known in the literature as "the logic of definedness", 
"E+-logic", etc., and are inspired by Bertrand Russell's classic 
analysis of definite descriptions. LPT has been fruitfully
applied in the foundations of mathematics by Michael Beeson, 
Solomon Feferman, William Farmer, and others, and more recently
David Parnas, the CoFI group, and others, have put LPT to use in the 
specification of computer systems. In LPT, functions and 
predicates are strict, and free variables are given the
generality interpretation. Both nonconstructive (classical) 
and constructive (intuitionist) brands of LPT have served in 
foundational investigations, and Hilbert-style
axiomatizations, natural deduction systems, and Gentzen-style
sequents have been developed for them. In this talk,
I provide an overview of nonconstructive LPT with definite 
descriptions, which I call LPD, and sketch some new results
regarding tableaux systems and the Craig Interpolation Lemma.
 
The inadequacy of LPT as the underlying first-order logic of 
specification languages and the description of an alternative 
logic more attune to computing practice will be the subject of 
Part II of this talk.
 
Reference: http://www.cs.uml.edu/~gumb/research/postscript/stab0.ps
 



 
  
 
 
  
  
 


 

Colloquium Coordinator: Jie Wang, wang@cs.uml.edu

Website: http://www.cs.uml.edu/~wang/colloquia/