TRANSPARENCIES FOR PANEL DISCUSSION 
	"LOGIC IN THE CS UNDERGRADUATE CURRICULUM"

SIGCSE CONFERENCE, Atlanta, February 28, 1998

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

Personal position:

		more than
			" logic is useful in CS "
		
		more than
			" logic is important for CS education "

	COMPUTER SCIENCE *IS* APPLIED LOGIC


Therefore

	A good computer scientist / applied logician

	MUST HAVE A LOGIC RELATED BASIC TRAINING

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

Logic comes historically from

	* Philosophical logic ( 2 millenia )

	* Mathematical logic ( 1 century )

	
A mixed blessing:

	POSITIVE

		provides impressive groundwork results

	NEGATIVE

		suggests that logic is imported to CS

	burdens CS-logic with off the mark traditions

		COMPUTER SCIENCE WOULD HAVE DISCOVERED
		AND DEVELOPED LOGIC IN ITS OWN IMAGE
		AS ITS CONCEPTUAL UNDERPINNING
		HAD LOGIC NOT BEEN THERE

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

LOGIC IS

	THE EXACT ANALYSIS OF GENERAL RULES

		relating
		
		MANIPULABLE FORM (syntax)

		with
		
		MEANING (semantics)

	CS IS THE FIRST SCIENCE WHERE THESE RELATIONS ARE CENTRAL,

	because

	*1*	Exact rules of form are essential
		for interpretation by machines

	*2*	Exact rules of meaning are essential
		because meaning is operational
		and of immediate importance

			[compare: natural / social / mathematical sciences]

	*3*	Exact rules can be feasibly manipulated

			( because there are machines to do it,
			  e.g. compilation )

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

THERE ARE 5 TYPES OF
	SYMBIOTIC RELATIONS BETWEEN
	LOGIC AND CS

	1. FUNDAMENTAL CONCEPTS

	2. FUNDAMENTAL CONSTRUCTS

	3. ANALYSIS AND APPLICATIONS

	4. ANALOGIES

	5. SYNTHESIS

	LOWER DIVISION UG EDUCATION
		IS CONCERNED WITH 1 & 2

	UPPER DIVISION INCLUDE SOME 3

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

FUNDAMENTAL CONCEPTS: ELEMENTARY EXAMPLES

	* INDUCTIVE GENERATION OF DATA

		=>	inductive proofs

			definition by recurrence

	E.G.

		0		x -> Sx			yield all N

		F[0]		F[x] -> F[Sx]		yield F [ all N ]

		f(0) dfnd	f(x) dfnd		yield  f [all N]
				     -> f(Sx) dfnd		    dfnd


	* DISTINCTIONS BETWEEN SYNTAX & SEMANTICS

	E.G.

		numerals	vs	natural numbers

		program text	vs	operational semantics		

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

FUNDAMENTAL CONCEPTS: "SOPHOMORE EXAMPLES"

	* PARSING	and other syntactic issues
			(binding, scope, transformations)

	* THE REGRESSIVE (= AXIOMATIC) METHODS

		BASIC vs DERIVED NOTIONS

			built-in functions vs programmed/dfnd functions

	* ABSTRACTION & ENCAPSULATION

			functionality, types

			procedures, modules, fnct dfntn

	* LEVELS OF DISCOURSE

		E.G.

			PARAMETERS vs variables

				A x^2 + B x + C = 0

			f(n) defnd by recursion

				vs

				f_n are defined by (discourse-level) recurrence

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

FUNDAMENTAL CONSTRUCT:
	EXAMPLES FROM PROGRAMMING LANG


	* FUNCTIONAL PROGRAMMING

		lambda calculus  =>  LISP, SCHEME ...

	* DECLARATIVE PROGRAMMING

		prolog ...

		higher order

	* RECURSIVE PROCEDURES

		syntax as data

		self reference


			MORE PROGRAMMING EXAMPLES:

				KIM BRUCE

			DATABASE & AI EXAMPLES:

				PHOKION KOLAITIS

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

FUNDAMENTAL CONSTRUCTS:
	EXAMPLES FROM COMPUTATION THEORY

	* BOOLEAN LOGIC, CIRCUITS

	* GRAMMARS, FORMAL LANGUAGES

	* FINITE STATE MACHINES, AUTOMATA THEORY

	* UNIVERSAL DEVICES, INTERPRETERS

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

ANALYSIS AND APPLICATIONS

	* FORMAL METHODS

		SPECIFICATIONS

			LANGUAGE SEMANTICS,
				COMPILER SEMANTICS

			SOFTWARE SPECS

			HARDWARE SPECS

			CO-SPECIFICATION

	* VERIFICATION

		LOGICS OF PROGRAMS

		PROGRAM DERIVATION AND INFERENCE

		MODEL CHECKING

	* AUTOMATED MATHEMATICS

		AUTOMAT, NuPRL, Mathematical Vernacular

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

ANALOGIES

	PRINCIPLES & METHODS WHICH
		UNIFY MATHEMATICA LOGIC AND CS LOGIC

	E.G. the SCH homomorphism

		PROOFS				PROGRAMS

	----------------------		----------------------

	    assumptions A ...		    variables  x:A ...

		...				...

	   natural deduction P		  functional prgrm P

		...				...

	    Theorem T			     if type T 

	----------------------		----------------------

			
	   HIGHER ORDER			    HIGHER ORDER
		LOGICS				TYPES
						(polymorphism)

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

SYNTHESIS: NEW DIRECTIONS

	E.G.

		* INFORMATION THEORY

		* VISUAL REASONING / PROGRAMMING

		* NOTIONS OF CERTAINTY & APPROXIMATION

			interactive proofs

			cryptography

		* LOGICS UNDERLYING DYNAMIC SYSTEMS

			biological systems
			
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=


FINAL MESSAGE

	DON'T 

		TEACH MATHEMATICAL LOGIC COURSE
			TO COMP SCI STUDENTS

	BUT DO

		* TEACH CS LOGIC COURSE

		* INTEGRATE LOGIC
			TO EXISTING COURSES