A Direct Proof of Hosoi's Theorem (Extended Abstract) (2015)
Amelia Harrison, Vladimir Lifschitz, David Pearce, and Agustin Valverde
The propositional logic of here-and-there, denoted by HT, is the superintuitionistic logic characterized by linearly ordered Kripke frames with two worlds (the "here" world and the "there" world). It was introduced by Arend Heyting [Heyting, 1930] as a tool for proving the independence of the law of the excluded middle. Recent interest in HT is related to its role in the theory of logic programming [Lifschitz et al., 2001].
In Abstracts of Papers Presented at the Third St. Petersburg Days of Logic and Computability 2015.

Amelia Harrison Ph.D. Student ameliaj [at] cs utexas edu
Vladimir Lifschitz Faculty vl [at] cs utexas edu