*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Tutorial 'Mechanised Reasoning in Economics' (Koblenz, Germany, 17 Sept.): early registration until 15 July*From*: Christoph LANGE <math.semantic.web at gmail.com>*Date*: Thu, 04 Jul 2013 23:08:16 +0100*Organization*: University of Birmingham*Sender*: Christoph Lange <allegristas at gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130627 Thunderbird/17.0.7

CALL FOR PARTICIPATION Applying Mechanised Reasoning in Economics – Making Reasoners Applicable for Domain Experts http://www.cs.bham.ac.uk/research/projects/formare/events/informatik2013/ Tutorial at Informatik 2013 – Computer science adapted to humans, organization and the environment, 43rd annual meeting of the German Informatics Society (Gesellschaft für Informatik e.V. (GI) http://informatik2013.de/ 17 September 2013, 14:00-17:30 Koblenz, Germany AUDIENCE Our audience comprises computer scientists developing or using mechanised reasoning systems, or interested in learning how to use them. The message of this tutorial is: 1. There are interesting nails (problems) out there in economics, waiting for hammers (tools) from computer science to be applied to them. 2. Those domain experts who have the interesting problems do not speak the same language as computer scientists do. 3. Therefore, it takes some effort to make computer science tools applicable in such domains: * giving meaningful feedback on errors, * writing application-oriented documentation, * trying hard to support users who understand textbook mathematics but not proof calculi, etc. MOTIVATION (ECONOMIST'S PERSPECTIVE) We have a vision of increasing confidence in economics' models and mechanisms. Auction designs are under constant evolution as they seek to incorporate lessons learned and to recognise specific features of the markets in which they are run. Similarly, current models for financial risk measurement are too large and change too quickly to be checked by hand. These challenges affect not only the economics sector itself, but also the government as it regulates the economy, and thus the general public. Since the software used is mission critical it should be verified to a high level of reliability. We believe that such problems can be addressed by representing the underlying knowledge in a formal, explicit way that is accessible to mechanised reasoning tools. These have already been applied to economics, albeit by computer scientists rather than the economists themselves. Many economists have postgraduate training in mathematics; historically, it has been less common for them to have training in computer science. Therefore, despite a growing interface (consider, e.g., the ACM Transactions on Economics and Computation), they lack awareness of the existence of reasoning tools and their appropriateness for tasks in economics. Moreover such tools are still challenging to use. The objective of our ForMaRE project (formal mathematical reasoning in economics) is to raise awareness and to enable economists to work with the languages and tools of their choice. RESEARCH CONTEXT (Computer Science Perspective) How can we make formal methods familiar to economists? Concretely, we are developing a basic Auction Theory Toolbox of formalisations, on top of which auction designers can formalise and verify their own auction designs, and we are getting started with applying similar techniques to matching markets and financial risk management. This tutorial reports on our experience and insights from carrying out this research. >From a computer science perspective, our “toolbox building” approach requires 1. identifying the right language to formalise the theory (i.e. being sufficiently expressive while still supporting efficient proofs), and 2. identifying a a mechanised reasoning system whose input and output are comprehensible to economists, who usually do pen-and-paper proofs and are familiar with mathematical textbook notation. We have so far gained experience with the languages/systems Isabelle/HOL and its jEdit IDE, Theorema, CASL and its Hets IDE and the System on TPTP web service, Mizar, as well as Prover9 and Mace4. * Economists may find it appealing that the structure of an Isabelle or Mizar proof resembles the structure of a paper proof, that Theorema is an add-on to the familiar Mathematica CAS with its textbook-like notebook interface, or that Hets allows for uniformly feeding one formalisation into a wide range of highly efficient automated theorem provers. * It may deter them that little documentation for these tools is available, or that it requires strong background knowledge, and that the investigation of unsuccessful automated proof attempts requires a good understanding of the underlying calculus. INTERACTIVE MATCHMAKING The last part of the tutorial involves an interactive matchmaking session. We will try to match tutorial participants who are developers or experienced users of tools (if you are, please contact us in advance!) and economics problems to which consider these tools may be applicable. We will briefly present the respective problem and ask the respective participant for a brief voluntary presentation of his or her tool. From our connections in the economics community (cf. our research collaborators and our organisation of the AISB 2013 symposium on Enabling Domain Experts to use Formalised Reasoning) we have a portfolio of around a dozen potentially matching problems. ORGANISERS * Christoph Lange, Computer Science, University of Birmingham, UK * Manfred Kerber, Computer Science, University of Birmingham, UK * Colin Rowat, Economics, University of Birmingham, UK Please contact us at formare-management at cs.bham.ac.uk. -- Christoph Lange, School of Computer Science, University of Birmingham http://cs.bham.ac.uk/~langec/, Skype duke4701 → Intelligent Computer Mathematics, 8–12 July, Bath, UK. http://cicm-conference.org/2013/ → Modular Ontologies (WoMO), 15 September, Corunna, Spain. Submission until 12 July; http://www.iaoa.org/womo/2013.html → Knowledge and Experience Management, 7-9 October, Bamberg, Germany. Submission until 15 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/ → Mathematics in Computer Science Special Issue on “Enabling Domain Experts to use Formalised Reasoning”; submission until 31 October. http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/

- Previous by Date: [isabelle] prove simple inequality
- Next by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Previous by Thread: Re: [isabelle] prove simple inequality
- Next by Thread: [isabelle] SMT and bound variables.
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list