Computer Science Logic: 12th International Workshop, CSL'98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings (Lecture Notes in Computer Science (1584))

This book constitutes the strictly refereed post-workshop proceedings of the 12th International Workshop on Computer Science Logic, CSL '98, held as the Annual Conference of the European Association on Computer Science Logic in Brno, Czech Republic in August 1998. The 25 revised full papers presented were carefully reviewed and selected during two rounds of reviewing and revision. Also included are three reviewed invited papers. The papers span the whole scope of computer science logic and mathematical foundations and represent the state of the art in the area. The 1998annual Conference Of The Europeanassociation For Computer Science Logic, Csl’98, Was Held In Brno, Czech Republic, During August 24-28, 1998. Csl’98wasthe12thinaseriesofworkshopsandthe7thtobeheldasthe Annual Conference Of The Eacsl. The Conference Was Organized At Masaryk University In Brno By The Faculty Of Informatics In Cooperation With Universities In Aaachen, Caen, Haagen, Linz, Metz, Pisa, Szeged, Vienna, And Other Institutions. Csl’98 Formed One Part Of A Federated Conferences Event, The Other Part Being Mfcs’98, The 23rd Int- National Symposium On The Mathematical Foundations Of Computer Science. This Federated Conferences Event Consisted Of Common Plenary Sessions, Invited Talks, Several Parallel Technical Programme Tracks, A Dozen Satellite Workshops Organized In Parallel, And Tutorials. The Federated Csl/mfcs’98 Conferences Event Included 19 Invited Talks, Four Of Them Joint Csl/mfcs’98 Talks (d. Harel, W. Maass, Y. Matiyasevic, And M. Yannakakis), Four For Csl (p. Hajek, J. Mitchell, Th. Schwentick, And J. Tiuryn), And Eleven For Mfcs. Last But Not Least, Two Tutorials Were Organized By Csl On The Day Preceding The Symposium On “inference Rules In Fragments Of Arithmetic” By Lev Beklemishev And On “proofs, Types, And Safe Mobile Code” By Greg Morrisett. A Total Of 345 Persons Attended The Federated Csl/mfcs’98 Conference Which Was A Great Success. The Program Committee Of Csl’98 Selected 27 Of 74 Papers Submitted For The Conference.from The 27 Papers Selected For Presentation,25 Havebeen Accepted, Following The Standard Refereeeing Procedure, For Publication In The Present P- Ceedings. Three Invited Speakers Submitted Papers, That Were Likewise Refereeed And Accepted. Invited Papers -- Trakhtenbrot Theorem And Fuzzy Logic -- Descriptive Complexity, Lower Bounds And Linear Time -- Testing Of Finite State Systems -- Contributed Papers -- On The Power Of Quantifiers In First-order Algebraic Specification -- On The Effective Semantics Of Nondeterministic, Nonmonotonic, Temporal Logic Databases -- Revision Programming = Logic Programming + Integrity Constraints -- Quantifiers And The System Ke: Some Surprising Results -- Choice Construct And Lindström Logics -- Monadic Np And Graph Minors -- Invariant Definability And P/poly -- Computational Complexity Of Ehrenfeucht-fraïssé Games On Finite Structures -- An Upper Bound For Minimal Resolution Refutations -- On An Optimal Deterministic Algorithm For Sat -- Characteristic Properties Of Majorant-computability Over The Reals -- Theorems Of Péter And Parsons In Computer Programming -- Kripke, Belnap, Urquhart And Relevant Decidability & Complexity -- Existence And Uniqueness Of Normal Forms In Pure Type Systems With ??-conversion -- Normalization Of Typable Terms By Superdevelopments -- Subtyping Functional+nonempty Record Types -- Monotone Fixed-point Types And Strong Normalization -- Morphisms And Partitions Of V-sets -- Computational Adequacy In An Elementary Topos -- Logical Relations And Inductive/coinductive Types -- On The Complexity Of H-subsumption -- Complexity Classes And Rewrite Systems With Polynomial Interpretation -- Rpo Constraint Solving Is In Np -- Quantifier Elimination In Fuzzy Logic -- Many-valued First-order Logics With Probabilistic Semantics. Georg Gottlob, Etienne Grandjean, Katrin Seyr (eds.). Includes Bibliographical References. Front Matter....Pages - Trakhtenbrot Theorem and Fuzzy Logic....Pages 1-8 Descriptive Complexity, Lower Bounds and Linear Time....Pages 9-28 Testing of Finite State Systems....Pages 29-44 On the Power of Quantifiers in First-Order Algebraic Specification....Pages 45-57 On the Effective Semantics of Nondeterministic, Nonmonotonic, Temporal Logic Databases....Pages 58-72 Revision Programming = Logic Programming + Integrity Constraints....Pages 73-89 Quantifiers and the System KE: Some Surprising Results....Pages 90-104 Choice Construct and Lindström Logics....Pages 105-125 Monadic NP and Graph Minors....Pages 126-141 Invariant Definability and P / poly ....Pages 142-158 Computational Complexity of Ehrenfeucht-Fraïssé Games on Finite Structures....Pages 159-170 An Upper Bound for Minimal Resolution Refutations....Pages 171-178 On an Optimal Deterministic Algorithm for SAT....Pages 179-187 Characteristic Properties of Majorant-Computability Over the Reals....Pages 188-203 Theorems of Péter and Parsons in Computer Programming....Pages 204-223 Kripke, Belnap, Urquhart and Relevant Decidability & Complexity....Pages 224-240 Existence and Uniqueness of Normal Forms in Pure Type Systems with βη -conversion....Pages 241-259 Normalization of Typable Terms by Superdevelopments....Pages 260-282 Subtyping Functional+Nonempty Record Types....Pages 283-297 Monotone Fixed-Point Types and Strong Normalization....Pages 298-312 Morphisms and Partitions of V -sets....Pages 313-322 Computational Adequacy in an Elementary Topos....Pages 323-342 Logical Relations and Inductive/Coinductive Types....Pages 343-354 On the Complexity of H-Subsumption....Pages 355-371 Complexity Classes and Rewrite Systems with Polynomial Interpretation....Pages 372-384 RPO Constraint Solving Is in NP....Pages 385-398 Quantifier Elimination in Fuzzy Logic....Pages 399-414 Many-Valued First-Order Logics with Probabilistic Semantics....Pages 415-429 Back Matter....Pages - These 25 refereed post workshop papers and three reviewed invited papers span the whole scope of computer science logic and mathematical foundations and represent the late 1990's "state of the art" in the area. It follows from Gödel's completeness theorem that the set of all tautologies of the classical (Boolean) predicate logic (denote this set by TAUTBool) is recursively enumerable, i. e.