Oct 19, 2010: Jaco van de Pol: Equational Logic Examples: Soundness and (In)Completeness

October 19, 2010Equational Logic Examples: Soundness and (In)Completeness
Room: Zi 5126Jaco van de Pol

The algebraic approach to mathematics and computer science is to define a structure of mathematical functions, and describe their relations by a number of equations. A popular question in this context is: "Can my theory be completely characterised by a finite set of equations, or not?". In this talk, I will discuss some basic observations, and give two recent examples: - a sound and complete axiomatization of sequential four-valued logic - a proof that a certain process algebra with priority cannot be finitely axiomatized. Along the way, I will show how an automated theorem prover helped me to settle a more than 10 years old open problem.