26 Computer Theorem Provers (CTPs \footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}) have a tradition as long as Computer Algebra Systems (CAS), another kind of mathematics assistants. However, CTPs task of proving is more challenging than calculating; so, in contrary to CASs, CTPs are not yet in widespread use --- not yet, because CTPs are on the step into industrial use in the current decade: Safe-critical software requires to be proven correct more and more \cite{db:dom-eng}, and the technology of CTP becomes ready to accomplish the task of efficiently proving hundreds of proof obligations. |
28 Computer Theorem Provers (CTPs \footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}) have a tradition as long as Computer Algebra Systems (CAS), another kind of mathematics assistants. However, CTPs task of proving is more challenging than calculating; so, in contrary to CASs, CTPs are not yet in widespread use --- not yet, because CTPs are on the step into industrial use in the current decade: Safe-critical software requires to be proven correct more and more \cite{db:dom-eng}, and the technology of CTP becomes ready to accomplish the task of efficiently proving hundreds of proof obligations. |
28 The present shift of the predominant user group from academic experts to software engineers raises novel user requirements for graphical user interfaces (GUI) of CTP. CTPs will become components of integrated development environments, and the knowledge bases have to scale up to industrial size. |
30 The present shift of the predominant user group from academic experts to software engineers raises novel user requirements for graphical user interfaces (GUI) of CTP. CTPs will become components of integrated development environments, and the knowledge bases have to scale up to industrial size. |