Journal
Scientific and technical journal of information technologies, mechanics and optics
UDK
Issue:6 (82)
Download PDF0 Kbyte
The article is devoted to a constructive proof (in Agda programming language) of the fact that Boolean formula satisfiability problem by means of sequent calculus and verification with CTL specifications can be implemented as structurally recursive dependently typed functions.