auto_awesome_motion View all 1 versions
organization

Lemma 1

Country: United Kingdom
4 Projects, page 1 of 1
  • Funder: UKRI Project Code: EP/J007498/1
    Funder Contribution: 389,556 GBP
    Partners: UQ, SU, University of Michigan–Flint, Articulate Software, JOHANNES KEPLER UNIVERSITAT LINZ UNIVERSITY OF LIN, Lemma 1, Miami University, University of Pennsylvania, University of Birmingham, JacobsUni

    This research applies methods and tools from mathematical knowledge management and theorem proving to theoretical economics, by working with a class of cooperative games called pillage games. Pillage games, introduced by Jordan in 2006, provide a formal way of thinking about the ability of powerful coalitions to take resources from less powerful ones. While their name suggests primitive, violent interactions, pillage games are more applicable to advanced democracies, in which coalitions seek to form governments to alter the distribution of society's resources in their favour. If, for some allocation of society's resources, the coalition preferring another allocation is stronger than that preferring the status quo, the other allocation `dominates' the status quo. The most conceptually intriguing, and the most computationally intractable solution concept for cooperative games is the `stable set'. A stable set, has two features: no allocation in the set dominates another; each allocation outside the set is dominated by an allocation in the set. For pillage games with three agents under a few additional conditions, we have determined when stable sets exist, that they are unique and contain no more than 15 allocations, and how to determine them for a given power function. In this research, we first formally represent the mathematical knowledge developed in Jordan's and our work using sTeX, a mathematical knowledge management tool. This allows, e.g., automatic identification of how various results depend on each other. We then use two modern automated theorem provers (ATPs), Isabelle and Theorema, to formally prove these results. Theorem proving is a hard task and if not provided with domain specific knowledge ATPs have to search through big search spaces in order to find proofs. To increase their reasoning power, we shall seek to identify recurring patterns in proofs, and extract proof tactics, reducing the interactions necessary to prove the theorems interactively. As important results in pillage games can be summarised in pseudo-algorithms, containing both computational and non-computational steps, we shall study such pseudo-algorithms, seeking to push them towards the much more efficient computational steps. Finally, we shall use the identified proof tactics to help the ATPs prove new results in order evaluate their true value. The research seeks to make a number of contributions. For theorem proving, pillage games form a new set of challenge problems. As the study of pillage games is new, and the canon of applicable knowledge small, this gives an unprecedented opportunity to encode most of it. The research will expand the tractable problem domain for ATPs; and - by identifying successful tactics - increase both the efficiency with which ATPs search for proofs, and - ideally - their ability to establish new results. For economics, this is the first major application of formal knowledge management and theorem proving techniques. The few previous applications of ATP to economics have formalised isolated results without engaging economists and have thus largely gone unnoticed by the discipline. As cooperative games are a known hard class of economic problems, and pillage games known to be tractable, this research therefore presents a strong `proof of concept' for the use of ATP within economics. Cooperative game theory is formally similar to graph theory, the techniques and insights developed may be applicable to matching problems, network economics, operations research, and combinatorial optimisation more generally. Additionally, the researchers will introduce ATP techniques to the leading PhD summer school in computational economics, and are working in collaboration with economic theorists with strong computational backgrounds. Thus, the research seeks to form a focal point for formal knowledge management and theorem proving efforts in economics.

  • Funder: UKRI Project Code: EP/N014758/1
    Funder Contribution: 1,304,450 GBP
    Partners: McAfee Labs, NHS Greater Glasgow and Clyde, Aristotle University of Thessaloniki, Scottish Government, Heriot-Watt University, NASA, Altran UK Ltd, D-RisQ Ltd, Osnabrück University, University of Trento...

    Our work in the DReaM group involves a unique blend of the techniques of artificial intelligence and theoretical computer science, enabling us to take a uniquely holistic perspective on automated reasoning and mathematical discovery. The proposed Platform Grant renewal will be used to provide essential infrastructure and to enable exploratory activities that will support a portfolio of projects which focus on the automation of mathematical reasoning processes, including their analysis, development and interaction. We can be broadly classified by our holistic perspective on automated reasoning. Central to this theme is the interplay between representation and reasoning. That is, discovering the right representation can often dramatically simplify the reasoning required in solving a problem, and conversely, meta-level reasoning, and in particular proof-failure analysis, can often provide guidance in evolving the right representations. The renewal of the Platform Grant will enable us to maintain and strengthen the momentum that has been built up around this theme - in terms of basic research as well as applications. The former covers a spectrum of topics, including: cognitive aspects of theory formation; mathematical discovery and automatic theorem generation; ontology creation, repair and evolution; proof procedures; computability; proof planning; AI problem reformulation; quantum computation; computational creativity; and the visualisation of reasoning processes. The latter covers wide ranging applications such as: software verification; formal modelling of software intensive systems; security and privacy analysis and design; graphic design; videogame design; disaster recovery planning; and the modelling of healthcare processes; poetry and art. The positive effective of our current Platform Grant funding can be seen across all aspects of our research - it enables us to: collaborate and exchange ideas with the best researchers in the world; explore and test new ideas; develop adventurous grant proposals and win funding; consolidate the results of our research projects and secure the follow-on funding that enables the impact of our research to be fully realised; and help develop the next generation of research stars and leaders in our field. A renewed Platform Grant would enable us to continue to grow as a research group, in terms of the career development of our researchers, the depth and breadth of our research, and the impact it has on wider aspects of society.

  • Funder: UKRI Project Code: EP/K040251/1
    Funder Contribution: 1,157,930 GBP
    Partners: Technology Dev Group BioDundee, D-RisQ Ltd, SU, MONO, Lemma 1, DECC, MICROSOFT RESEARCH LIMITED, IBM (United Kingdom), UWO, LMS...

    Mathematics is a profound intellectual achievement with impact on all aspects of business and society. For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. "Crowdsourcing" pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers check proofs that are just too long and complicated for any human to comprehend, using programs designed to verify hardware. Yet these techniques are currently used in stand-alone fashion, lacking integration with each other or with human creativity or fallibility. Social machines are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity. Our long-term vision is to change mathematics, transforming the reach, pace, and impact of mathematics research, through creating a mathematics social machine: a combination of people, computers, and archives to create and apply mathematics. Thus, for example, an industry researcher wanting to design a network with specific properties could quickly access diverse research skills and research; explore hypotheses; discuss possible solutions; obtain surety of correctness to a desired level; and create new mathematics that individual effort might never imagine or verify. Seamlessly integrated "under the hood" might be a mixture of diverse people and machines, formal and informal approaches, old and new mathematics, experiment and proof. The obstacles to realising the vision are that (i) We do not have a high level understanding of the production of mathematics by people and machines, integrating the current diverse research approaches (ii) There is no shared view among the diverse re- search and user communities of what is and might be possible or desirable The outcome of the fellowship will be a new vision of a mathematics social machine, transforming the reach, pace and impact of mathematics. It will deliver: analysis and experiment to understand current and future production of mathematics as a social machine; designs and prototypes; ownership among academic and industry stakeholders; a roadmap for delivery of the next generation of social machines; and an international team ready to make it a reality.

  • Funder: UKRI Project Code: EP/K040251/2
    Funder Contribution: 1,146,390 GBP
    Partners: Lemma 1, MONO, MICROSOFT RESEARCH LIMITED, IBM (United Kingdom), JacobsUni, University of Oxford, D-RisQ Ltd, UWO, Institute of Mathematics and its Applica, SU...

    Mathematics is a profound intellectual achievement with impact on all aspects of business and society. For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. "Crowdsourcing" pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers check proofs that are just too long and complicated for any human to comprehend, using programs designed to verify hardware. Yet these techniques are currently used in stand-alone fashion, lacking integration with each other or with human creativity or fallibility. Social machines are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity. Our long-term vision is to change mathematics, transforming the reach, pace, and impact of mathematics research, through creating a mathematics social machine: a combination of people, computers, and archives to create and apply mathematics. Thus, for example, an industry researcher wanting to design a network with specific properties could quickly access diverse research skills and research; explore hypotheses; discuss possible solutions; obtain surety of correctness to a desired level; and create new mathematics that individual effort might never imagine or verify. Seamlessly integrated "under the hood" might be a mixture of diverse people and machines, formal and informal approaches, old and new mathematics, experiment and proof. The obstacles to realising the vision are that (i) We do not have a high level understanding of the production of mathematics by people and machines, integrating the current diverse research approaches (ii) There is no shared view among the diverse re- search and user communities of what is and might be possible or desirable The outcome of the fellowship will be a new vision of a mathematics social machine, transforming the reach, pace and impact of mathematics. It will deliver: analysis and experiment to understand current and future production of mathematics as a social machine; designs and prototypes; ownership among academic and industry stakeholders; a roadmap for delivery of the next generation of social machines; and an international team ready to make it a reality.