Computational Logic and Proof Theory: 5th Kurt Gödel Colloquium, KGC ’97 Vienna, Austria, August 25–29, 1997 Proceedings

Leo Bachmair (auth.), Georg Gottlob, Alexander Leitsch, Daniele Mundici (eds.)9783540633853, 3-540-63385-5

This book constitutes the refereed proceedings of the 5th Kurt Gödel Colloquium on Computational Logic and Proof Theory, KGC ’97, held in Vienna, Austria, in August 1997.
The volume presents 20 revised full papers selected from 38 submitted papers. Also included are seven invited contributions by leading experts in the area. The book documents interdisciplinary work done in the area of computer science and mathematical logics by combining research on provability, analysis of proofs, proof search, and complexity.

---

Table of contents :
Paramodulation, superposition, and simplification….Pages 1-3
Explaining Gentzen’s consistency proof within infinitary proof theory….Pages 4-17
Alogtime algorithms for tree isomorphism, comparison, and canonization….Pages 18-33
Ultrafilter logic and generic reasoning….Pages 34-53
Informal rigor and mathematical understanding….Pages 54-64
Resolution, inverse method and the sequent calculus….Pages 65-83
Subtyping over a lattice (abstract)….Pages 84-88
A new method for bounding the complexity of modal logics….Pages 89-102
Parameter free induction and reflection….Pages 103-113
Looking for an analogue of Rice’s Theorem in circuit complexity theory….Pages 114-127
Two connections between Linear Logic and Łukasiewicz Logics….Pages 128-139
Structuring of computer-generated proofs by cut introduction….Pages 140-152
NaDSyL and some applications….Pages 153-166
Markov’s rule is admissible in the set theory with intuitionistic logic….Pages 167-171
Bounded hyperset theory and web-like data bases….Pages 172-185
Invariant definability….Pages 186-202
Comparing computational representations of Herbrand models….Pages 203-218
Restart tableaux with selection function….Pages 219-232
Two semantics and logics based on the Gödel interpretation….Pages 233-240
On the completeness and decidability of a restricted first order linear temporal logic….Pages 241-254
Propositional quantification in intuitionistic logic….Pages 255-263
Sketch-as-proof….Pages 264-277
Translating set theoretical proofs into type theoretical programs….Pages 278-289
Denotational semantics for polarized (but-non-constrained) LK by means of the additives….Pages 290-304
The undecidability of simultaneous rigid E -unification with two variables….Pages 305-318
The tangibility reflection principle for self-verifying axiom systems….Pages 319-334
Upper bounds for standardizations and an application….Pages 335-348