摘要: INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program s correctness which are supported respectively by the mechanized logics—FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system: the rules,implementation,tactics,forward proof and backward proof.It also gives several typical exam- pies for demonstration of INCAPS worki…