Theorem proving in higher order logics. 11th international conference, TPHOLs '98. Canberra, Australia, September 27 - October 1, 1998. Proceedings (Q1269998)

The articles of mathematical interest will be reviewed individually. The preceding conference (9th, 1996) has been announced (see Zbl 0852.00020). Indexed articles: \textit{Caldwell, James L.}, Classical propositional decidability via Nuprl proof extraction, 105-122 [Zbl 0927.03016] \textit{Harrison, John}, Formalizing basic first order model theory, 153-170 [Zbl 0930.03010] \textit{Howe, Douglas J.}, A type annotation scheme for Nuprl, 207-224 [Zbl 0927.03020] \textit{Konrad, Karsten}, HOT: A concurrent automated theorem prover based on higher-order tableaux, 245-261 [Zbl 0927.03021] \textit{Liang, Chuck}, Free variables and subexpressions in higher-order meta logic, 263-276 [Zbl 0927.03053] \textit{Lifantsev, Maxim; Bachmair, Leo}, An LPO-based termination ordering for higher-order terms without \(\lambda\)-abstraction, 277-293 [Zbl 0927.03054] \textit{Mikhajlova, Anna; von Wright, Joakim}, Proving isomorphism of first-order logic proof systems in HOL, 295-314 [Zbl 0927.03023] \textit{Müller, Olaf}, I/O automata and beyond: Temporal logic and abstraction in Isabelle, 331-348 [Zbl 0927.03024] \textit{Naraschewski, Wolfgang; Wenzel, Markus}, Object-oriented verification based on record subtyping in higher-order logic, 349-366 [Zbl 0927.03026] \textit{Sawamura, Hajime; Asanuma, Daisaku}, Mechanizing relevant logics with HOL, 443-460 [Zbl 0927.03028]