Computational logic and proof theory. 5th Kurt Gödel Colloquium, KGC '97. Vienna, Austria. August 25--29, 1997. Proceedings (Q1365518)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Buchholz, Wilfried}, Explaining Gentzen's consistency proof within infinitary proof theory, 4-17 [Zbl 0887.03043] \textit{Buss, Samuel R.}, Alogtime algorithms for tree isomorphism, comparison, and canonization, 18-33 [Zbl 0884.68098] \textit{Carnielli, W. A.; Veloso, P. A. S.}, Ultrafilter logic and generic reasoning, 34-53 [Zbl 0884.03024] \textit{Robinson, J. A.}, Informal rigor and mathematical understanding, 54-64 [Zbl 0886.03002] \textit{Tammet, Tanel}, Resolution, inverse method and the sequent calculus, 65-83 [Zbl 0888.03004] \textit{Tiuryn, Jerzy}, Subtyping over a lattice, 84-88 [Zbl 0885.03016] \textit{Basin, David; Matthews, Seán; Viganò, Luca}, A new method for bounding the complexity of modal logics, 89-102 [Zbl 0886.03039] \textit{Beklemishev, Lev D.}, Parameter free induction and reflection, 103-113 [Zbl 0892.03023] \textit{Borchert, Bernd; Stephan, Frank}, Looking for an analogue of Rice's theorem in circuit complexity theory, 114-127 [Zbl 0894.03020] \textit{Ciabattoni, Agata; Luchi, Duccio}, Two connections between linear logic and Łukasiewicz logics, 128-139 [Zbl 0884.03052] \textit{Egly, Uwe; Genther, Karin}, Structuring of computer-generated proofs by cut introduction, 140-152 [Zbl 0885.03012] \textit{Gilmore, Paul C.}, NaDSyL and some applications, 153-166 [Zbl 0885.03025] \textit{Khakhanian, V. Kh.}, Markov's rule is admissible in the set theory with intuitionistic logic, 167-171 [Zbl 0881.03031] \textit{Makowsky, J. A.}, Invariant definability. (Extended abstract), 186-202 [Zbl 0881.03022] \textit{Matzinger, Robert}, Comparing computational representation of Herbrand models, 203-218 [Zbl 0885.03013] \textit{Pape, Christian; Hähnle, Reiner}, Restart tableaux with selection function, 219-323 [Zbl 0887.03007] \textit{Plisko, V.}, Two semantics and logics based on the Gödel interpretation, 233-240 [Zbl 0893.03021] \textit{Pliuškevičius, Regimantas}, On the completeness and decidability of a restricted first order linear temporal logic, 241-254 [Zbl 0885.03020] \textit{Połacik, Tomasz}, Propositional quantification in intuitionistic logic, 255-263 [Zbl 0887.03003] \textit{Preining, Norbert}, Sketch-as-proof, 264-277 [Zbl 0944.03053] \textit{Setzer, Anton}, Translating set theoretical proofs into type theoretical programs, 278-289 [Zbl 0884.03054] \textit{Tortora de Falco, Lorenzo}, Denotational semantics for polarized (but-non-constrained) \(LK\) by means of the additives, 290-304 [Zbl 0884.03053] \textit{Veanes, Margus}, The undecidability of simultaneous rigid \(E\)-unification with two variables, 305-318 [Zbl 0884.03047] \textit{Willard, Dan E.}, The tangibility reflection principle for self-verifying axiom systems, 319-334 [Zbl 0884.03056] \textit{Xi, Hongwei}, Upper bounds for standardizations and an application, 335-348 [Zbl 0888.03006]