Algebraic process theories, also known as process algebras, are
prototype specification languages for reactive systems---that is, for
devices that compute by reacting to stimuli from their environment.
The main strength of such theories lies in the equational
(calculational) style of reasoning they support. For each
process theory, several natural questions immediately arise pertaining
to the (non-)existence of (finite or recursive) sets of laws that
allow one to prove by "substituting equals for equals" all of the
valid equalities between process descriptions (closed or open terms)
over fragments of the process theory at hand.
Currently, answering such questions is only possible via delicate,
error-prone and lengthy proofs. This project aims at establishing a
generic framework for answering such questions efficiently and at
applying the proposed general theory to solve some of the main open
problems in the study of the equational logic of processes.