Break through result

Oliver Kullmann and his co-authors Marein Heule, and Victor Marek used SAT-solving techniques to solve a long standing open problem in Ramsey Theory known as the Boolean Pythagorean Triples Problem: It is impossible to divide the natural numbers into two parts such that none of the parts contains a Pythagorean triple, that is numbers a,b,c such that a^2+b^2=c^2. In fact, they found a smallest number N (namely N = 7825) such that the set {1,…,N} cannot be divided into two parts as described above. Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek. Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. In Nadia Creignou and Daniel Le Berre (Ed.), Theory and Applications of Satisfiability Testing – SAT 2016. (pp. 228-245). Springer.



Wordpress is loading infos from uni-trier

Please wait for API server to collect data from

Computing with Infinite Data EU Horizon 2020 Marie Sklodowska-Curie Research and Innovation Staff Exchange (MSCA-RISE), 4 years, start April 2017, total value 1,462,500 Euros Participating universities Siegen (Germany), Trier(Germany), Munich (Germany), Swansea (UK), Birmingham (UK), INRIA (France), Ljubljana (Slovenia), Maastricht (Netherlands), Stockholm (Sweden), Padova (Italy), Algarve (Portugal), Aston (UK), Dortmund(Germany), KAIST (Korea), JAIST (Japan), Novosibirsk (Russia), UNISA (South-Africa), Andres Bello (Chile), Canterbury (NZ), Cincinnati (USA), Nanyang (Singapore), Abstract The joint research in this programme will study important aspects—both theoretical as well as applied—of computing with infinite objects. A central aim is laying the grounds for the generation of efficient and verified software in engineering applications. A prime example for infinite data is provided by the real numbers, most commonly conceived as infinite sequences of digits. While most applications in science and engineering substitute the reals with floating point numbers of fixed finite precision and thus have to deal with truncation and rounding errors, the approach in this project is different: exact real numbers are taken as first-class citizens and while any computation can only exploit a finite portion of its input in finite time, increased precision is always available by continuing the computation process. This project aims to bring together the expertise of specialists in mathematics, logic, and computer science to push the frontiers of our theoretical and practical understanding of computing with infinite objects. Three overarching motivations drive the proposed collaboration: Representability. Cardinality considerations tell us that it is not possible to represent arbitrary mathematical objects in a way that is accessible to computation. We will enlist expertise in topology, logic, and set theory, to address the question of which objects are representable and how they can be represented most efficiently. Constructivity. Working in a constructive mathematical universe can greatly enhance our understanding of the link between computation and mathematical structure. It not only informs us which are the objects of relevance, it also allows us to devise always correct algorithms from proofs. Efficient implementation. We also aim to make progress on concrete implementations. Theoretical insights from elsewhere will be tested in actual computer systems; obstacles encountered in the latter will inform the direction of mathematical investigation.  


Hideki Tsuiki visiting

Hideki Tsuiki from Kyoto University is visiting Swansea from 15 to 28 August 2016. He is an expert in Domain Theory, Effective Topology and Exact Real Number Computation. He is working with Ulrich Berger and the Munich Minlog group on the Extraction of infinity Gray code for real numbers.

New research project DETIPS

Markus Roggenbach and John Tucker, in collaboration with their colleagues Mark Jones and Xianghia Xie from the Visual Computing Group were awarded an EPSRC grant for their research project Data Release – Trust, Identity, Privacy and Security (DETIPS).   


Data Release – Trust, Identity, Privacy and Security Mark Jones (PI), Markus Roggenbach, John Tucker and Xianghua Xie (CoIs) EPSRC grant The Open Data Initiative (ODI) demonstrates that there is a growing ambition from government to publish internal data as open data sets. (See Data custodians, particularly large governmental organisations such as the DVLA and HMRC, have a legal duty, enforced by the Information Commissioner’s Office (ICO), and social duty of care to the public, to ensure that privacy is not breached by the release of data as open data sets. These large organisations face an increasingly difficult task in establishing whether the release of data will result in enough data being open to triangulate individuals and destroy privacy. Our research takes a collaborative approach uniquely combining formal methods, counter-fraud, data mining and data visualization to produce new tools, methodologies and theory for working with data release. We will produce tools that allow interactive analysis of data sets to determine if data release can combine with existing data to triangulate personal data. We will take a new approach of using formal notions about data, memorandums of understanding (of data use) and criteria of control to auto-generate software tools that allow the user to manipulate, investigate and analyse data sets for potential unintended consequences if released. We will undertake empirical studies with data keepers, data users and members of the public to inform data policies surrounding release of data and integrate this within our toolsets and methodologies.


Nao Hirokawa visiting

Nao Hirokawa from the Japan Advanced Institute of Science and Technology (JAIST) is visiting Swansea from 15 to 17 March. Nao is an expert in Term rewriting theory. The abstract of his seminar talk about Basic Normalization on Thursday, 15 March can be found here.