Gentzen’s se­quent cal­cu­lus is a foun­da­tion of mod­ern logic and, more re­cently, pro­gram­ming lan­guage de­sign. It is known for being more sym­met­ric than nat­ural de­duc­tion, a de­duc­tion cal­cu­lus that is bi­ased on proofs and truth, whereas se­quent cal­cu­lus does sym­met­ri­cally sup­port proofs/truth and refu­ta­tions/fal­sity.

How­ever, the way se­quent cal­cu­lus is usu­ally de­fined, those sym­me­tries have to be ob­served and proved after the fact, as op­posed to be an in­her­ent part of the cal­cu­lus.

Our re­search group has de­vel­oped a method of syn­tac­ti­cally ab­stract­ing over so-called po­lar­i­ties and ori­en­ta­tions. The task of this the­sis is to 1) apply this method to the se­quent cal­cu­lus and Her­be­lin’s pro­gram­ming cal­cu­lus based on the se­quent cal­cu­lus, and 2) val­i­dat­ing the new for­mu­la­tion by show­ing that proofs and pro­grams can be “poly­mor­phic” in their po­lar­ity and ori­en­ta­tion.

Fur­ther In­for­ma­tion

• Wikipedia Entry on Se­quent Cal­cu­lus
• Tu­to­r­ial on Se­quent Cal­cu­lus and re­lated pro­gram­ming cal­culi

Con­tact

Klaus Os­ter­mann