Equational reasoning

headed by Prof. Dr. Gerard R. Renardel de Lavalette

Equational reasoning is a well-known kind of mathematical reasoning that is practised e.g. in algebra and in many correctness proofs. Its standard formalisation is equational logic, a simple but very general reasoning system that is often used in computing science, e.g. in algebraic specification and rewrite systems (Mathematica is a well-known example). Proof theory for this logic, addressing structural properties of equational proofs, hardly exists, and we try to fill in the gap.