Abstract. Subtropical real root finding is a heuristic method designed to solve large multivariate polynomials. This method considers the polynomial as a collection of exponent vectors associated with sign information on the coefficients. It employs linear programming to heuristically identify points where the values of the polynomial have opposite signs. In successful cases, the intermediate value theorem is utilized to compute a zero of the polynomial represented as a tuple of real algebraic numbers. By implementing this approach using the Reduce computer algebra system and theGurobi LP solver, we have achieved success in solving hundreds of problems derived from established mathematical models in chemistry and systems biology. These problems involved polynomials with up to 800,000 monomials in 10 variables and degrees up to 12, with an incompleteness failure rate of approximately 10 percent.

The method has been adapted to satisfiability modulo theories solving (SMT), where the focus went from one single polynomial equation to several simultaneous strict polynomial inequalities. We found that such problems represent more than 40 percent of the QF_NRA section of the SMT-LIB library of benchmarks. Technically, input problems in the theory QF_NRA are reduced problems in QF_LRA. Then SMT itself can be used in place of LP solving, which admits linear problems that are not necessarily pure conjunctions of constraints. Systematic experiments on the SMT-LIB have shown that the method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques.

The talk gives an overview of the method and its application, along with theoretical results regarding its incompleteness.

Abstract.  Rewriting is a formalism widely used in computer science and mathematical logic. The classical formalism has been extended, in the context of functional languages, with an order over the rules and, in the context of rewrite based languages, with the negation over patterns. We have proposed a concise and clear algorithm computing the difference over patterns which can be used to define generic encodings of constructor term rewriting systems with negation and order into classical term rewriting systems. As a direct consequence, established methods used for term rewriting systems can be applied to analyze the properties of the extended systems. The approach can also be seen as a generic compiler which targets any language providing basic pattern matching primitives. The formalism provides also a new method for deciding if a set of patterns subsumes a given pattern and thus, for checking the completeness of a set of patterns, the presence of useless patterns, or the absence of some patterns. The latter is particularly useful when one wants to verify that some patterns are absent from the result of a particular transformation and several extensions have been proposed to statically verify the absence of specified patterns from the reachable terms of constructor based term rewriting systems.

Abstract. TLA+ is a language for the formal description of (mainly) concurrent and distributed algorithms and systems, based on Zermelo-Fraenkel set theory and linear-time temporal logic. Verifying properties of TLA+ specifications is supported by model checking (TLC and Apalache) and by theorem proving (TLAPS). This tutorial will provide an introduction to the language and its accompanying tools, using the problem of distributed termination detection as a running example.

Abstract. Some interesting problems have a poor worst-case complexity, but may still be soluble in some, or many, cases. If appropriate, there is ‘fixed-parameter tractability’ as one way of describing the solubility. But in other cases, e.g. SAT-solving, there isn’t necessarily a neat theoretical solution, but powerful practical ideas. What can we say about problems around real quantifier elimination?

In 1922, a young 21-year-old Curry started reading Principia Mathematica and was intrigued by the complications of its substitution rule. As a result of trying to analyse substitution, Curry conceived of the combinators in 1926 and started a lifelong search for powerful systems that combine computations and deductions (functions and logic) and that are able to formalise mathematics. His formalisms as well as existing complementary and competing formalisms demonstrate the struggle to internalise as much as possible while keeping the system consistent. There is also a struggle for elegant theories that minimise the number of basic concepts while remaining as close as possible to the language’s structure, and also the struggle for generalising concepts, connecting areas that may seem far apart and applying useful techniques from one area to the other.

This talk discusses two aspects of this development:

• First, we go back as far as the ancient mathematicians (and especially the Pythagorean school) and discuss how the problems/paradoxes associated with of the infinite led them to miss the opportunity of defining the real numbers and how the developments from middle ages to the 17th and 19th century led to the development of real numbers and mathematical analysis, and also to even more paradoxes that led to the birth of computability and mathematical foundations.
• Second, we discuss the problem of defining and internalising substitution in the lamba calculus and how to avoid the hurdle of how/when to introduce the substitution rule and alpha congruence. We cannot define alpha congruence without a form of substitution but for substitution and reduction to work, we need to assume a form of alpha congruence. The Curry school of thought has laid the foundations for this.

There is also a third aspect which discusses the struggle of going fully formal (especially with the variety and approaches to mechanise and formalise mathematics, e.g., in proof checkers) and keeping the informal as well as the historical tradition and lessons.

Abstract.  SNP systems are known as a class of distributed parallel neural-like computation models, which are inspired by the mechanism that biological neurons process information and communicate with each other by means of spikes. In the past decade, the neurons in particular and the brain in general have been investigated and better understood in part also due to the two major projects: Human Brain Project in Europe and BRAIN Initiative (US). We will present several results related to the SNP systems and their variations as computing devices, in many cases achieving Turing Universality even in restricted cases. Recent research results and open questions will also be presented especially for the Spiking neural P systems with communication on request (SNQ P systems). We are able to construct small Turing universal SNQ P systems by using low numbers of neurons. Specifically, a Turing universal SNQ P system as number generating devices (resp., number accepting devices and function computing devices) is constructed by using 12 (resp., 11 and 21) neurons.

Abstract. The useful information carried by spatio-temporal data is often outlined by geometric structures and patterns. Filaments or clusters induced by galaxy positions in our Universe are such an example. Two situations are to be considered. First, the pattern of interest is hidden in the data set, hence the pattern should be detected. Second, the structure to be studied is observed, so relevant characterization of it should be done. Probabilistic modelling is one of the approaches that allows to furnish answers to these questions. This is done by developing unitary methodologies embracing simultaneously three directions: modelling, simulation, and inference. This talk presents the use of marked point processes applied to such structures detection and characterization. Practical examples are also shown.