From Philosophical to Industrial Logics

One of the surprising developments in the area of program verification is how ideas introduced by logicians in the early part of the 20th Century ended up yielding by the 21 Century industrial-standard property-specification languages. This development was enabled by the equally unlikely transformation of the mathematical machinery of automata on infinite words, introduced in the early 1960s for second-order logic, into effective algorithms for model-checking tools. This paper attempts to trace the tangled threads of this development. 1 Thread I: Classical Logic of Time

• Type: Conference
• Year: 2009
• Where: ICLA
• Authors: Moshe Y. Vardi
• Keywords: Artificial Intelligence, Century Industrial-standard Property-specification, ICLA 2009, Second-order Logic, Surprising Developments