Computer science logic

More about the book

Inhaltsverzeichnis includes invited lectures on various topics such as interactive and geometric characterizations of proof spaces, the symbolic approach to repeated games, and the relationship between proofs, programs, and abstract complexity. It covers model-checking first-order logic, automata, and locality, as well as the exchange rates between automata. The discussion includes precise relational invariants via strategy iteration, logic and games, and omega-regular half-positional winning conditions. It also examines clique-width and parity games, logical refinements of Church’s problem, and the expressive power of counting logics on restricted finite structures. The content compares expressive power in well-structured transition systems and explores the existence of certain ?-powers of any Borel rank. It addresses satisfiability in spatial logic with tree variables, forest expressions, and MSO on infinite binary trees. The annotation highlights classical and intuitionistic logic, qualitative temporal and spatial reasoning, and the integration of linear arithmetic into superposition calculus. Further discussions include lambda calculus, effective lambda models, typed normal form bisimulation, and classical program extraction. The structure theorem for FO2 on words and the complexity of reasoning about dynamic policies are also covered. The text delves into linear logic, focusing proofs, and proof theory while incorpora