Algebraic Gentzen systems
for partially ordered algebraic systems
The corresponding notion
in logic has been very successful for formulating and implementing
decision procedures for a large number of logics.
A Gentzen rule is a quasi-inequality of the form
where the `s_i,t_i`,`s,t` are terms.
Rules with `n=0` are called
Gentzen rules are usually written in the form
A simple example of a Gentzen system is given by the following
These four rules give a decision procedure for the equational theory
If we want to decide if `s(x)<=t(x)`, match any
conclusion of these rules to this inequality, and repeat this step
with the premises of the rule.
If there is some choice of rules that
always ends with instances of the axiom `x<=x`, the inequality holds,
and otherwise it fails.
Of course deciding semilattice equations is trivial, but this set of
rules can be easily extended to cover
lattices by adding the following three rules:
In fact this is a version of Whitman's solution of the word problem in