Fangzhen Lin: A formalization of programs in first-order logic with a discrete linear order. Artif. Intell. 235: 1-25 (2016)