PQDR:
Probabilistic, Quantum and Differential Reasoning
A project of SQIG at IT awaiting support.
Everybody who has worked in formal logic will confirm that it is one of the technically most refractory parts of mathematics. The reason for this is that it deals with rigid, all-or-none concepts, and has very little contact with the continuous concept of the real or of complex number, that is, with mathematical analysis. Yet analysis is the technically most successful and best-elaborated part of mathematics. Thus formal logic is, by the nature of its approach, cut off from the best cultivated portions of mathematics, and forced onto the most difficult part of the mathematical terrain, into combinatorics.
John von Neumann, The General and Logic Theory of Automata, in L. A Jeffress (ed.), Cerebral Mechanisms in Behavior: The Hixon Symposium, New York, John Whiley, 1951, pag 406.
Team Coordinators
Key publications
-
A. Sernadas, J. Rasga, C. Sernadas, and P. Mateus. Approximate reasoning about logic circuits with single-fan-out unreliable gates. Preprint, SQIG - IT and IST - TU Lisbon, 1049-001 Lisboa, Portugal, 2013. Submitted for publication. Preprint: 13-SRSM-pcl04.pdf
-
J. Rasga, W. Lotfallah, and C. Sernadas. Completeness and interpolation of almost-everywhere quantification over finitely additive measures. Mathematical Logic Quarterly, in print. Preprint: 13-RLS-folae.pdf
Summary
Mathematical logic was first developed by mathematicians concerned with the consistency of Mathematics. After some initial successes, Hilbert's program of formalizing mathematics for making sure that no such inconsistencies exist came to an abrupt end with Gödel's incompleteness theorems. However, the effort was not lost on several accounts. First, it contributed to the latest information revolution (the advent of the universal computer). Second, several useful fragments of Mathematics have been shown to be decidable (e.g. real closed fields). Third, several interesting results have been proved with the techniques of Mathematical Logic (e.g. independence theorems). Fourth, Mathematical Logic born out of pure math concerns soon became an active field of applied math (e.g. in Artificial Intelligence, Software Engineering).
In recent developments of Applied Mathematical Logic, it has become clear the need for capturing in decidable (or at least semi-decidable) formal systems knowledge about quantitative aspects of the universe of discourse at hand. For instance, one may be interested in the probability of a formula being true. More recently, the quantization drive expanded to other quantitative aspects of reality, including time and space. For instance, for verifying an air traffic control system one needs a formal system capable of reasoning about continuous variables and their derivatives over time. The interest on quantum computation triggered by Shor's algorithm put up yet another challenge to the applied logicians.
The project addresses some of the problems arising in the quantization of logic. As such, it is naturally organized into five tasks, as follows:
- Task 1: Design a probabilistic logic for reasoning about circuits with faulty gates, proving its weak completeness and providing meaningful applications in circuit design. The full study of this logic will follow (namely addressing interpolation, decidability and complexity of model checking and satisfiability). The analysis of sub-circuit reuse (with gate fan outs >1) is also an objective. Afterwards, a logic for reasoning about quantum circuits with faulty gates will also be developed.
Team: Amílcar Sernadas; Cristina Sernadas; João Rasga; Paulo Mateus.
- Task 2: (i) Develop logics for reasoning about quantum security. (ii) Propose quantum algorithms for SAT. Concerning (i), first a Hoare logic for the verification of single-thread quantum protocols will be developed and afterwards a dependent-type system for the verification of multi-thread quantum protocols will be investigated. Regarding (ii), the aim is the development of a quantum adiabatic algorithm for SAT of probabilistic logics, exploring the fact that probabilistic models can be represented efficiently with quantum states.
Team: Amílcar Sernadas; André Souto; Jaime Ramos; João Rodrigues; Manuel Biscaia; Paulo Mateus; Pedro Baltazar; Ricardo Loura.
- Task 3: Bring probabilistic reasoning into the usual symbolic methods for analyzing security
protocols, thus strengthening the standard Dolev-Yao attacker beyond state-of-the-art tools. The proposed development will be anchored on a suitable logical foundation, combining equational reasoning with a variant of probabilistic dynamic epistemic logic and focused on concrete applications, including off-line guessing and other computational indistinguishability notions.
Team: Andreia Mordido; Carlos Caleiro; Jaime Ramos; Paula Gouveia; Pedro Adão; Pedro Baltazar; Sérgio Marcelino.
- Task 4: Add probabilistic (and maybe quantum) features both on logics for hybrid systems and on o-minimal hybrid systems. The enrichment of the logics with structured data having a decidable theory is also envisaged, as well as proving the decidability of many-sorted combinations of such theories. Constructive reasoning on differential equations is also a concern capitalizing on a constructive proof of quantifier elimination for the theory of differential closed fields.
Team: Amílcar Sernadas; Cristina Sernadas; David Henriques; Jaime Ramos; João Rasga; Paulo Mateus.
- Task 5: Investigate from a computability and complexity perspective the arising problems: (i) when digital computers are used in applications involving real numbers; and (ii) in non-conventional models of computation over the real numbers. Problems related to dynamical systems theory are envisaged in (i). Concerning (ii), the idea is to compare some of those computational models with Turing machines in order to understand whether one can expect or not computational gains.
Team: Amaury Pouly; Amílcar Sernadas; Cláudia Philippart; Daniel Graça; João Rasga; Pedro Baltazar.
