公理系の形式化やら、機械的に証明可能な定理の構成やらを、
機械的に行う試みは、まだまだ一般化されていないと思うわけだが。