A system for modelling and proving circuits

摘要

We present the architecture of FORMATH, a system for modelling andproving circuits. Its core is a formal system, the P-calculus whichallows one to accurately describe structures and behaviours of circuits.In order to perform verifications, the P-calculus is implemented intoproof assistants