摘要: 在用重写系统描述逻辑位，门电路，位串和自然数的基础上，对半加器，全加器和串行加法器等基本硬件电路的逻辑功能进行了刻画，并用基于重写归纳的推理技术证明了所有描述的正确性，为用重写技术正确描述和验证复杂硬件电路奠定了基础。最后给出与其他类似工作的分析和比较。