Ordering is a well-established concept in mathematics and also plays an important role in many areas of computer science, where quasi-orderings , most notably well-founded quasi-orderings and well-quasi-orderings, are of particular interest. This paper deals with quasi-orderings on first-order terms and introduces a new notion of unification based on a special quasi-order, known as homeomorphic tree embedding . Historically, the development of unification theory began with the central notion of a most general unifier based on the subsumption order . A unifier $\sigma$ is most general, if it subsumes any other unifier $\tau$ , that is, if there is a substitution $\lambda$ with $\tau=_{E}\sigma\lambda$ , where E is an equational theory and $=_{E}$ denotes equality under E. Since there is in general more than one most general unifier for unification problems under equational theories E, called E-Unification , we have the notion of a complete and minimal set of unifiers under E for a unification problem $\varGamma$ , denoted as $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ . This set is still the basic notion in unification theory today. But, unfortunately, the subsumption quasi-order is not a well-founded quasi-order, which is the reason why for certain equational theories there are solvable E-unification problems, but the set $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ does not exist. They are called type nullary in the unification hierarchy. In order to overcome this problem and also to substantially reduce the number of most general unifiers, we extended the well-known encompassment order on terms to an encompassment order on substitutions (modulo E). Unification under the encompassment order is called essential unification and if $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ exists, then the complete set of essential unifiers $e\mathcal{U}\Sigma_{E}(\Gamma)$ is a subset of $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ . An interesting effect is that many E-unification problems with an infinite set of most general unifiers (under the subsumption order) reduce to a problem with only finitely many essential unifiers. Moreover, there are cases of an equational theory E, for which the complete set of most general unifiers does not exist, the minimal and complete set of essential unifiers however does exist. Unfortunately again, the encompassment order is not a well-founded quasi-ordering either, that is, there are still theories with a solvable unification problem, for which a minimal and complete set of essential unifiers does not exist. This paper deals with a third approach, namely the extension of the well-known homeomorphic embedding of terms to a homeomorphic embedding of substitutions (modulo E) . We examine the set of most general, minimal, and complete E-unifiers under the quasi-order of homeomorphic embedment modulo an equational theory E, called $\varphi U\Sigma_{E}(\Gamma)$ , and propose an appropriate definitional framework based on the standard notions of unification theory extended by notions for the tree embedding theorem or Kruskal’s theorem as it is called. The main results are that for regular theories the minimal and complete set $\varphi\mathcal{U}\Sigma_{E}(\Gamma)$ always exists. If we restrict the E-embedding order to pure E-embedding, a well-known technique in logic programming and term rewriting where the difference between variables is ignored, the set $\varphi_{\pi}\mathcal{U}\Sigma_{E}(\Gamma)$ always exists and it is even finite for any theory E.

The risk of an accidental nuclear war has increased greatly in recent years. Developments in computer science and artificial intelligence (AI) contribute to the potential danger, since early warning and decision support systems (EWDS) are based on very complex computer systems and networks for predicting and evaluating possible attacks by nuclear missiles. This may involve false alarms caused by sensors, hardware or software failures. Errors in the interpretation, processing, or routing of data can lead to a false attack message and thus to a very critical situation. In particular, an EWDS may contain AI-based functions that automatically make decisions for certain subtasks, which can be wrong. Cyberattacks can also have dangerous and incalculable interactions with early warning and decision-making systems, significantly increasing the risk of a nuclear war by accident.

In these days of exuberant fantasies about the future development of artificial intelligence-mostly written by people who have never in their lives developed an AI program-the GFFT (Society for the Promotion of Technology Transfer) has also unleashed a competition on future AI scenarios to honour Wolfgang Bibel. Because I was allowed to give the laudatory speech for Wolfgang, I was also asked to contribute something to the pen. And because, despite everything else, it is not reprehensible to think about the future, I could not refrain from doing so. Here is my somewhat expanded contribution.

We want to use the 22nd of January 2021 as an opportunity to honor the “ Treaty on the Prohibition of Nuclear Weapons ”, TPNW, by this article, as the treaty will enter into force on this day.

A unifier of two terms s and t is a substitution sigma such that s sigma = t sigma. For first-order terms there exists a most general unifier sigma in the sense that any other unifier tau can be composed from sigma with some substitution lambda such that tau = sigma circle lambda. For many practical applications it turned out to be useful to generalize this notion to E-unification, where E is an equational theory, = (E) is equality under E and sigma is an E-unifier if s sigma = (E) t(sigma). Depending on the equational theory E, the set of most general unifiers is always a singleton (as above) or it may have more than one unifier, either finitely or infinitely many unifiers and for some theories it may not even exist, in which case we call the theory of type nullary. The set of most general unifiers is denoted as mu u Sigma(E)(Gamma) for a unification problem Gamma, which is a system of equations and an equational theory E. Unfortunately the set mu u Sigma(E)(Gamma) may be very large in general-even if it is finite-and for all practical purposes not really useful. For this and other reasons there is hence (i) a strong interest to compute a much smaller generating set of minimal unifiers and then (ii) to find efficient engineering solutions to handle these sets. Essential unifiers, as introduced by Hoche and Szabo, generalize the notion of a most general unifier and they have a dramatically pleasant effect: the set of essential unifiers is often much smaller than the set of most general unifiers. Essential unification may even reduce an infinitary theory to an essentially finitary theory. For example the one variable string unification problem is essentially finitary whereas it is infinitary in the usual sense. The most drastic reduction known so far is obtained for idempotent semigroups, or bands as they are called in computer science, which are of type nullary: there exist two unifiable terms s and t, but the set of most general unifiers does not exist. This is in stark contrast to essential unification: the set of essential unifiers for bands always exists and is finite. The key idea for essential unification is to base the notion of generality not on the standard subsumption order for terms with the associated subsumption order for substitutions, but on the encompassment order for terms and substitutions. Hence we propose the encompassment order as a more natural order relation for minimal and complete sets of E-unifiers and call these sets essential unifiers, denoted as mu u Sigma(E)(Gamma). This paper introduces essential unification, provides a definitional framework based on order relations and surveys what is presently known. We conclude with a list of some of the more important open problems, including the main open problem, namely how to build essential unification into an automated reasoning system.

This volume contains selected and revised versions of papers that were presented at two of the workshops held at the 14th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2011) on November 14, 2011, in Wollongong, Australia. PRIMA is one of the oldest active agent computing forums, beginning in 1998 as a regional agent workshop (the Pacific Rim International Workshop on Multi-Agents). Alongside the main conference, PRIMA includes workshops that are intended to facilitate active exchange, interaction and comparison of approaches, methods and various ideas in specific areas related to intelligent agent systems and multiagent systems. In alignment with the conference theme for PRIMA 2011 of Agents for Sustainability, the 2011 workshop program sought to encourage thought leadership in the agent community as to how agent computing can be applied to enhance sustainable practices in our world, from agriculture and personal resource usage to the design and operation of more sustainable cities.

This series of volumes, the first covering 1957 and 1966 and the second 1967 to 1970, contains those papers which have shaped and influenced the field of computational logic and makes available the classical work, which in many cases is difficult to obtain or had not previously appeared in English. The main purpose of this series is to evaluate the ideas of the time and to select those papers, which can now be regarded as classics after more than a decade of intensive research.

Mathematics is the lingua franca of modern science, not least because of its conciseness and abstractive power. The ability to prove mathematical theorems is a key prerequisite in many fields of modern science, and the training of how to do proofs therefore plays a major part in the education of students in these subjects. Computer-supported learning is an increasingly important form of study since it allows for independent learning and individualised instruction.

This volume contains the Proceedings of the 7th International Conference on Text, Speech and Dialogue, held in Brno, Czech Republic, in September 2004, under the auspices of the Masaryk University. Th

The traditional view of an algorithm A is that it is a recipe, a sequence of exact steps designed to facilitate the execution of some goal involving, say, an entity E. This view goes back to the Greeks with such well known examples as Euclid’s algorithm and can be found even earlier in the Babylonian times. It is the view that has been taken up ever since by mathematicians and more recently in computer science: myriads of such algorithms are known and recorded. General investigations tried to make these notions precise and the last century in particular turned out to be very fruitful indeed with the foundational work in mathematics and computer science. So, for example if E is a list and we wish to order it according to some measure, we may have a rich choice of algorithms for achieving this goal. They may differ in style and efficiency. Taking this view of an algorithm A, two properties come immediately to mind.

The ΩMEGA project and its predecessor, the MKRP-system, grew out of the principal dissatisfaction with the methodology and lack of success of the search-based "logic engines" of the 1960s and 1970s.

The lives of mathematical prodigies who passed away very early after groundbreaking work invoke a fascination for later generations: The early death of Niels Henrik Abel (1802–1829) from ill health after a sled trip to visit his fiancé for Christmas; the obscure circumstances of Evariste Galois’ (1811–1832) duel; the deaths of consumption of Gotthold Eisenstein (1823–1852) (who sometimes lectured his few students from his bedside) and of Gustav Roch (1839–1866) in Venice; the drowning of the topologist Pavel Samuilovich Urysohn (1898–1924) on vacation; the burial of Raymond Paley (1907–1933) in an avalanche at Deception Pass in the Rocky Mountains; as well as the fatal imprisonment of Gerhard Gentzen (1909–1945) in Prague — these are tales most scholars of logic and mathematics have heard in their student days. Jacques Herbrand, a young prodigy admitted to the École Normale Supérieure as the best student of the year 1925, when he was 17, died only six years later in a mountaineering accident in La Bérarde (Isère) in France. He left a legacy in logic and mathematics that is outstanding. Inevitably, when all introductory words are said in the annual postgraduate course on logic and automated deduction, the professor will feel the urge to point out to the young students that there are things beyond the latest developments of computer technology or the fabric of the Internet: eternal truths valid on planet Earth but in all those far away galaxies just as well. And as there are still ten minutes to go till the end of the lecture, the students listen in surprise to the strange tale about the unknown flying objects from the far away, now visiting planet Earth and being welcomed by a party of human dignitaries from all strata of society. Not knowing what to make of all this, the little green visitors will ponder the state of evolution on this strange but beautiful planet: obviously life is there — but can it think?

A unifier of two terms s and t is a substitution sigma such that s sigma = t sigma and for first-order terms there exists a most general unifier sigma in the sense that any other unifier delta can be composed from sigma with some substitution lambda, i.e. delta = sigma omicron lambda.For many practical applications it turned out to be useful to generalize this notion to E-unification, where E is an equational theory, = (E) is equality under E and sigma is an E-unifier if s sigma = (E) t sigma. Depending on the equational theory E, the set of most general unifiers is always a singleton (as above) or it may have more than one unifier, either finitely or infinitely many unifiers and for some theories it may not even exist, in which case we call the theory of type nullary.String unification (or Lob's problem, Markov's problem, unification of word equations or Makanin's problem as it is often called in the literature) is the E-unification problem, where E = {f(x, f(y, z)) = f(f(x, y), z)}, i.e. unification under associativity or string unification once we drop the fs and the brackets. It is well known that this problem is infinitary and decidable.Essential unifiers, as introduced by Hoche and Szabo, generalize the notion of a most general unifier and have a dramatically pleasant effect in the sense that the set of essential unifiers is often much smaller than the set of most general unifiers. Essential unification may even reduce an infinitary theory to an essentially finitary theory. The most dramatic reduction known so far is obtained for idempotent semigroups or bands as they are called in computer science: bands are of type nullary, i.e. there exist two unifiable terms s and t, for which the complete and minimal set of most general unifiers does not exist. This is in stark contrast to essential unification: the set of essential unifiers for bands always exists and is finite.We show in this paper that string unification in one variable, known to be infinitary, has a finite number of essential unifiers (i.e. is e-finitary), however the early hope for a similar reduction of unification under associativity is not justified: string unification is essentially infinitary. We give an enumeration algorithm for essential unifiers.