nach oben

2020 | Buch

Fields of Logic and Computation III

Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday

herausgegeben von: Prof. Dr. Andreas Blass, Patrick Cégielski, Nachum Dershowitz, Prof. Dr. Manfred Droste, Prof. Bernd Finkbeiner

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This Festschrift is published in honor of Yuri Gurevich’s 80th birthday. An associated conference, YuriFest 2020, was planned for May 18–20 in Fontainebleau, France, in combination with the 39th Journées sur les Arithmétiques Faibles also celebrating Yuri’s 80th birthday. Because of the coronavirus situation, the conference had to be postponed, but this Festschrift is being published as originally planned. It addresses a very wide variety of topics, but by no means all of the fields of logic and computation in which Yuri has made important progress.

Inhaltsverzeichnis

Frontmatter

On Yuri Gurevich

Frontmatter

To Yuri at 80 and More than 40 Years of Friendship

Abstract

An after-dinner speech for Yuri Gurevich’s 80th birthday.

Johann A. Makowsky

Technical Papers

Frontmatter

State of the Art in Logics for Verification of Resource-Bounded Multi-Agent Systems

Abstract

Approaches to the verification of multi-agent systems are typically based on games or transition systems defined in terms of states and actions. However such approaches often ignore a key aspect of multi-agent systems, namely that the agents’ actions require (and sometimes produce) resources. We survey previous work on the verification of multi-agent systems that takes resources into account, extending substantially a survey from 2016 [9].

Natasha Alechina, Brian Logan

Why Predicative Sets?

Abstract

The predicativist program for the foundations of mathematics, initiated by Poincaré and first developed by Weyl, seeks to establish certainty in mathematics without revolutionizing it. The program was later extensively pursued by Feferman, who developed proofs systems for predicative mathematics, and showed that a very large part of classical analysis can be developed within them. Both Weyl and Feferman worked within type-theoretic frameworks. In contrast, set theory is almost universally accepted now as the foundational theory in which the whole of mathematics can and should be developed. We explain how to reconstruct Weyl’s ideas and system within the set-theoretical framework, and indicate the advantages that this approach to predicativity and to set theory has from both the foundational as well as the computational points of views.

Arnon Avron

Functional Thesauri, Classifying Topoi, Unification, and Flatness

Abstract

We describe a part of the theory of classifying topoi and its connections with various topics from computer science, logic, and algebra.

Andreas Blass

Parameterized Parallel Computing and First-Order Logic

Abstract

The relationship between the complexity class \(\mathrm{AC}^0\) and first-order logic transfers to the parameterized class \(\mathrm {para}\text {-}\mathrm{AC}^0\), the parameterized analogue of \(\mathrm{AC}^0\). In the last years this relationship has turned out to be very fruitful. In this paper we survey some of the results obtained, mainly applications of logic to complexity theory. However the last section presents a strict hierarchy theorem for first-order logic obtained by a result of complexity theory.

Yijia Chen, Jörg Flum

Betweenness in Order-Theoretic Trees

Abstract

The ternary betweenness relation of a tree, B(x, y, z), indicates that y is on the unique path between x and z. This notion can be extended to order-theoretic trees defined as partial orders such that the set of nodes greater than any node is linearly ordered. In such generalized trees, the unique “path” between two nodes can have infinitely many nodes.

We generalize some results obtained in a previous article for the betweenness of join-trees. Join-trees are order-theoretic trees such that any two nodes have a least upper-bound. The motivation was to define conveniently the rank-width of a countable graph. We have called quasi-tree the betweenness relation of a join-tree. We proved that quasi-trees are axiomatized by a first-order sentence.

Here, we obtain a monadic second-order axiomatization of betweenness in order-theoretic trees. We also define and compare several induced betweenness relations, i.e., restrictions to sets of nodes of the betweenness relations in generalized trees of different kinds. We prove that induced betweenness in quasi-trees is characterized by a first-order sentence. The proof uses order-theoretic trees.

Bruno Courcelle

Relativization of Gurevich’s Conjectures

Abstract

Gurevich [6] conjectured that there is no logic for \(\textsf {P}\) or for \(\textsf {NP} \cap \textsf {coNP}\). For the latter complexity class, he also showed that the existence of a logic would imply that \(\textsf {NP} \cap \textsf {coNP}\) has a complete problem under polynomial time reductions. We show that there is an oracle with respect to which \(\textsf {P}\) does have a logic and \(\textsf {P}\ne \textsf {NP}\). We also show that a logic for \(\textsf {NP} \cap \textsf {coNP}\) follows from the existence of a complete problem and a further assumption about canonical labelling. For intersection classes \(\varSigma _n^p \cap \varPi _n^p\) higher in the polynomial hierarchy, the existence of a logic is equivalent to the existence of complete problems.

Anatole Dahan, Anuj Dawar

Seventy Years of Computer Science

Abstract

A quick tour through my long career with emphasis on how computer science has affected me and how I have affected computer science.

Martin Davis

Convergence and Nonconvergence Laws for Random Expansions of Product Structures

Abstract

We prove (non)convergence laws for random expansions of product structures. More precisely, we ask which structures \({\mathfrak A}\) admit a limit law, saying that the probability that a randomly chosen expansion of \({\mathfrak A}^n\) satisfies a fixed first-order sentence always converges when n approaches infinity. For the groups \({\mathbb Z}_p\), where p is prime, we do indeed have such a limit law, even for the infinitary logic \(L^\omega _{\infty \omega }\), and these probabilities always converge to dyadic rational numbers, whose denominator only depends on the expansion vocabulary. This can be used to prove that the Abelian group summation problem is not definable in \(L^\omega _{\infty \omega }\). Further examples for structures with such a limit law are permutation structures and structures whose vocabulary only consists of monadic relations. As a negative example, we prove that the very simple structure \((\{0,1\}, \le )\) does not have a limit law. Furthermore, we develop a method based on positive primitive interpretations that allows transferring (non)convergence results to other structures. Using this method, we are able to prove that structures with binary function symbols or unary functions that are not interpreted by permutations do not have a limit law in general.

Anuj Dawar, Erich Grädel, Matthias Hoelzel

Medieval Arabic Notions of Algorithm: Some Further Raw Evidence

Abstract

During YuriFest 2010 the discovery of a proof search algorithm devised in the 1020s by Ibn Sīnā (Avicenna) was announced. A Gurevich abstract state machine was given in evidence that Ibn Sīnā really did intend an algorithm; this was needed because Ibn Sīnā explained the algorithm by a long sequence of exercises, not by a rigorous definition. More recently a radically original logical decision algorithm has come to light in the work of the 12th century Baghdad scholar Abū al-Barakāt. Taking these algorithms alongside the already known algorithms of al-Khwārizmī for solving quadratic equations, and of al-Khalīl for listing finite sequences of letters, we can see that the medieval Arabic scholars uncovered a range of algorithms of various kinds. But it seems that they never brought these algorithms together under a single notion of ‘algorithm’; in fact we know of no writer who drew a comparison between any two of these algorithms. A natural question for historical research is to uncover what kinds of entity the medieval Arabic scholars thought these algorithms were. The present paper assembles some raw material that should be relevant to this question, including a not very successful attempt by al-Fārābī to institute a theory of logical procedures.

Wilfrid Hodges

On the Generalized Membership Problem in Relatively Hyperbolic Groups

Abstract

The aim of this note is to provide a proof of the decidability of the generalized membership problem for relatively quasi-convex subgroups of finitely presented relatively hyperbolic groups, under some reasonably mild conditions on the peripheral structure of these groups. These hypotheses are satisfied, in particular, by toral relatively hyperbolic groups.

Olga Kharlampovich, Pascal Weil

Identities of the Kauffman Monoid and of the Jones Monoid

Abstract

Kauffman monoids \(\mathcal {K}_n\) and Jones monoids \(\mathcal {J}_n\), \(n=2,3,\dots \), are two families of monoids relevant in knot theory. We prove a somewhat counterintuitive result that the Kauffman monoids \(\mathcal {K}_3\) and \(\mathcal {K}_4\) satisfy exactly the same identities. This leads to a polynomial time algorithm to check whether a given identity holds in \(\mathcal {K}_4\). As a byproduct, we also find a polynomial time algorithm for checking identities in the Jones monoid \(\mathcal {J}_4\).

Nikita V. Kitov, Mikhail V. Volkov

Relativistic Effects Can Be Used to Achieve a Universal Square-Root (Or Even Faster) Computation Speedup

Abstract

In this paper, we show that special relativity phenomenon can be used to reduce computation time of any algorithm from T to \(\sqrt{T}\). For this purpose, we keep computers where they are, but the whole civilization starts moving around the computers – at an increasing speed, reaching speeds close to the speed of light. A similar square-root speedup can be achieved if we place ourselves near a growing black hole. Combining the two schemes can lead to an even faster speedup: from time T to the 4-th order root \(\root 4 \of {T}\).

Olga Kosheleva, Vladik Kreinovich

Towards Verifying Logic Programs in the Input Language of clingo

Abstract

We would like to develop methods for verifying programs in the input language of the answer set solver clingo using software created for the automation of reasoning in first-order theories. As a step in this direction, we extend Clark’s completion to a class of clingo programs that contain arithmetic operations as well as intervals and prove that every stable model is a model of generalized completion. The translator anthem calculates the completion of a program and represents it in a format that can be processed by first-order theorem provers. Some properties of programs can be verified by anthem and the theorem prover vampire, working together.

Vladimir Lifschitz, Patrick Lühne, Torsten Schaub

Computing on Lattice-Ordered Abelian Groups

Abstract

Starting from a classical theorem of Gurevich and Kokorin we survey recent diverging developments of the theories of lattice-ordered abelian groups and their counterparts equipped with a distinguished order unit. We will focus on decision and recognition problems. As an application of Elliott’s classification, we will touch on word problems of AF C*-algebras.

Daniele Mundici

The Expressive Power of Temporal and First-Order Metric Logics

Abstract

The First-Order Monadic Logic of Order (\(\textit{FO}[<] \)) is a prominent logic for the specification of properties of systems evolving in time. The celebrated result of Kamp [14] states that a temporal logic with just two modalities Until and Since has the same expressive power as \(\textit{FO}[<] \) over the standard discrete time of naturals and continuous time of reals. An influential consequence of Kamp’s theorem is that this temporal logic has emerged as the canonical Linear Time Temporal Logic (\( LTL )\). Neither \( LTL \) nor \(\textit{FO}[<] \) can express over the reals properties like P holds exactly after one unit of time. Such local metric properties are easily expressible in \(\textit{FO}[<,+1] \) - the extension of \(\textit{FO}[<] \) by +1 function. Hirshfeld and Rabinovich [10] proved that no temporal logic with a finite set of modalities has the same expressive power as \(\textit{FO}[<,+1] \).

\(\textit{FO}[<,+1] \) lacks expressive power to specify a natural global metric property “the current moment is an integer.” Surprisingly, we show that the extension of \(\textit{FO}[<,+1] \) by a monadic predicate “x is an integer” is equivalent to a temporal logic with a finite set of modalities.

Alexander Rabinovich

Two First-Order Theories of Ordinals

Abstract

This paper compares a first-order theory of ordinals proposed by the author to the theory published 1965 by Gaisi Takeuti. A clarification of the relative deductive strength of the two theories is obtained.

Peter H. Schmitt

Randomness Tests: Theory and Practice

Abstract

The mathematical theory of probabilities does not refer to the notion of an individual random object. For example, when we toss a fair coin n times, all \(2^n\) bit strings of length n are equiprobable outcomes and none of them is more “random” than others. However, when testing a statistical model, e.g., the fair coin hypothesis, we necessarily have to distinguish between outcomes that contradict this model, i.e., the outcomes that convince us to reject this model with some level of certainty, and all other outcomes. The same question arises when we apply randomness tests to some hardware random bits generator.

A similar distinction between random and non-random objects appears in algorithmic information theory. Algorithmic information theory defines the notion of an individual random sequence and therefore splits all infinite bit sequences into random and non-random ones. For finite sequences there is no sharp boundary. Instead, the notion of randomness deficiency can be defined, and sequences with greater deficiency are considered as “less random” ones. This definition can be given in terms of randomness tests that are similar to the practical tests used for checking (pseudo)random bits generators. However, these two kinds of randomness tests are rarely compared and discussed together.

In this survey we try to discuss current methods of producing and testing random bits, having in mind algorithmic information theory as a reference point. We also suggest some approach to construct robust practical tests for random bits.

Alexander Shen

On Entropic Convergence of Algorithms

Abstract

The paper describes an approach to measuring convergence of an algorithm to its result in terms of an entropy-like function of partitions of its inputs of a given length. It is a way to relate the set-theoretic definition of a function to the program that computes it. The approach, though very preliminary, may show how to improve a given algorithm.

Anatol Slissenko

The Power of Spreadsheet Computations

Abstract

We investigate the expressive power of spreadsheets. We consider spreadsheets which contain only formulas, and assume that they are small templates, which can be filled to a larger area of the grid to process input data of variable size. Therefore we can compare them to well-known machine models of computation. We consider a number of classes of spreadsheets defined by restrictions on their reference structure. Two of the classes correspond closely to parallel complexity classes: we prove a direct correspondence between the dimensions of the spreadsheet and amount of hardware and time used by a parallel computer to compute the same function. As a tool, we describe spreadsheets which are universal in these classes, i.e. can emulate any other spreadsheet from them. In other cases we provide spreadsheet implementations of a solver for a polynomial-time complete problem, which indicates that the such spreadsheets are unlikely to have efficient parallel evaluation algorithms. Thus we get a picture how the computational power of spreadsheets depends on their dimensions and structure of references.

Jerzy Tyszkiewicz

Non-Algorithmic Theory of Randomness

Abstract

This paper proposes an alternative language for expressing results of the algorithmic theory of randomness. The language is more precise in that it does not involve unspecified additive or multiplicative constants, making mathematical results, in principle, applicable in practice. Our main testing ground for the proposed language is the problem of defining Bernoulli sequences, which was of great interest to Andrei Kolmogorov and his students.

Vladimir Vovk

Backmatter

Titel: Fields of Logic and Computation III
herausgegeben von: Prof. Dr. Andreas Blass
Patrick Cégielski
Nachum Dershowitz
Prof. Dr. Manfred Droste
Prof. Bernd Finkbeiner
Verlag: Springer International Publishing
Electronic ISBN: 978-3-030-48006-6
Print ISBN: 978-3-030-48005-9
DOI: https://doi.org/10.1007/978-3-030-48006-6