Effective temporal logics of programs
Hajnal Andréka, Valentin Goranko, Szabolcs Mikulás, Istvàn Németi, Ildikó Sain · 2019
In this chapter we investigate effective proof systems for temporal logics both propositional and first-order. The issue of effective proof systems for propositional temporal logic is much easier than for the first-order one. Partly because of this and partly because of applications we dwell on the first-order case much longer than on the propositional case. We prove soundness and completeness theorems for various effective proof systems and compare the program verifying - power of those systems.