You can subscribe to this list here.
2009 
_{Jan}

_{Feb}

_{Mar}
(6) 
_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}
(4) 
_{Nov}

_{Dec}
(6) 

2010 
_{Jan}
(5) 
_{Feb}

_{Mar}
(2) 
_{Apr}
(4) 
_{May}

_{Jun}

_{Jul}

_{Aug}
(6) 
_{Sep}
(3) 
_{Oct}

_{Nov}

_{Dec}

2012 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}
(3) 
_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

2013 
_{Jan}
(12) 
_{Feb}
(2) 
_{Mar}

_{Apr}
(1) 
_{May}
(2) 
_{Jun}
(1) 
_{Jul}

_{Aug}

_{Sep}

_{Oct}
(1) 
_{Nov}

_{Dec}

2014 
_{Jan}
(1) 
_{Feb}

_{Mar}

_{Apr}

_{May}
(4) 
_{Jun}
(6) 
_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

From: Michael Shulman <shulman@sa...>  20140618 05:02:48

From: Ken Monks <ken.monks@gm...>  20140612 06:15:02

From: Michael Shulman <shulman@sa...>  20140604 06:13:29

Thanks very much for your long and helpful explanation! It might be nice (although I'm sure you have plenty of other things to do) to put a bit of this explanation into the "Ruleset  Number Theory" topic, in case other users have a similar reaction to mine. I'm excited to hear that you have plans for adding typed expressions to Lurch. I am a big fan of typetheoretic foundations for mathematics, both practically and pedagogically. (Now that you point out the complete untypedness of Lurch, I see that you can even prove something nonsensical like "contradiction >= 0" by induction.) If you have time, I'd be interested to hear what sort of type system you have in mind. Of course, many "realworld" computer proof assistants are based on some kind of type theory. While I understand Lurch is intended only as a pedagogical tool, it would be nice if it could also provide a smooth bridge to "professional" proof assistants, for students who are interested in pursuing that direction. Your comments also prompt me to ask another question: for what level(s) of logic courses are you and others using Lurch? Some of the material on the web site suggested to me that they were courses in *formal* logic, which I would expect to be upperdivision courses. But you said in your last email that your students are seeing induction for the first time, which makes it sound instead like you're teaching an "introduction to proofs" class. Or do you use it for both types of courses? Mike PS. In case it would help to know my background: I've been doing a lot of research recently on dependent type theories and getting to know my way around proof assistants like Coq and Agda, and I've come to think that some sort of computer help would also be very valuable to my students struggling to come to grips with the concept of proof. I was pointed to Lurch by a comment at http://matheducators.stackexchange.com/questions/224/teachinglogicwithaproofassistant , and I'm very excited by it. I'm in the exploringoptions stages for an "introduction to proofs" class that I'll be teaching in Spring 2015. 
From: Ken Monks <ken.monks@gm...>  20140603 20:11:24

From: Ken Monks <ken.monks@gm...>  20140603 18:01:15

Thank you for sharing this very helpful information! We will try to automate as much of this as possible for linux users and post it to our site. KEN On Sat, May 31, 2014 at 3:14 PM, Michael Shulman <shulman@...> wrote: > Hi! > > After much effort, I think I have managed to install Lurch on Ubuntu > 12.04. There are four problems I ran into: > > 1. The download page > https://sourceforge.net/projects/lurch/files/Lurch/0.8/ doesn't seem > to include a Linux script for version 0.8. > > 2. Qt5 doesn't appear to be present in 12.04. Searching the Internet > led me to > http://askubuntu.com/questions/279421/howcaniinstallqt5xon1204lts > which instructed me to "aptaddrepository ppa:ubuntusdkteam/ppa" > and then install "qtdeclarative5dev". I then had to run "qmake" > rather than "qmakeqt5". > > 3. Cloning the lurch git repository didn't also clone the submodule > qtmathjax and the subsubmodule MathJax. > > 4. I needed to install several additional development packages: > qtscript5dev, libqt5webkit5dev, and libsqlite3dev. > > Now it works! > > Problem 1 could probably be fixed easily. Problem 3 should be fixable > by using "git clone recursive" in the install script. And Problem 4 > should be fixable by installing the necessary packages in the install > script. (Of course, there might also be other packages that need to > be installed, but were automatically pulled in for me by > qtdeclarative5dev; it might be better to install only the actually > required packages rather than a large bundle.) > > I'm not so sure about Problem 2. It probably isn't an issue in newer > versions of Ubuntu (except for the naming of qmake), and I'm not sure > whether the script could test for an older version and automatically > add a PPA if needed. But the script could at least give the user some > instructions about the required steps, e.g. if qmake is not found or > has the wrong version then it could say "If you're running an older > version of Ubuntu, you may need to do the following..." > > I'm looking forward to exploring Lurch! > > Best regards, > Mike > > >  > Time is money. Stop wasting it! Get your web API in 5 minutes. > http://www.restlet.com/download > http://p.sf.net/sfu/restlet > _______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss > 
From: Michael Shulman <shulman@sa...>  20140602 21:37:02

I think there is a bug in the definition of induction in the "Ruleset  Number Theory" included with Lurch: the variable n in the conclusion, as well as the variable k in the inductive hypothesis, should be restricted to be a natural number. Otherwise one can, say, prove by induction that \forall n,0\leq n, and then instantiate n by 1. 
From: Michael Shulman <shulman@sa...>  20140531 19:15:21

Hi! After much effort, I think I have managed to install Lurch on Ubuntu 12.04. There are four problems I ran into: 1. The download page https://sourceforge.net/projects/lurch/files/Lurch/0.8/ doesn't seem to include a Linux script for version 0.8. 2. Qt5 doesn't appear to be present in 12.04. Searching the Internet led me to http://askubuntu.com/questions/279421/howcaniinstallqt5xon1204lts which instructed me to "aptaddrepository ppa:ubuntusdkteam/ppa" and then install "qtdeclarative5dev". I then had to run "qmake" rather than "qmakeqt5". 3. Cloning the lurch git repository didn't also clone the submodule qtmathjax and the subsubmodule MathJax. 4. I needed to install several additional development packages: qtscript5dev, libqt5webkit5dev, and libsqlite3dev. Now it works! Problem 1 could probably be fixed easily. Problem 3 should be fixable by using "git clone recursive" in the install script. And Problem 4 should be fixable by installing the necessary packages in the install script. (Of course, there might also be other packages that need to be installed, but were automatically pulled in for me by qtdeclarative5dev; it might be better to install only the actually required packages rather than a large bundle.) I'm not so sure about Problem 2. It probably isn't an issue in newer versions of Ubuntu (except for the naming of qmake), and I'm not sure whether the script could test for an older version and automatically add a PPA if needed. But the script could at least give the user some instructions about the required steps, e.g. if qmake is not found or has the wrong version then it could say "If you're running an older version of Ubuntu, you may need to do the following..." I'm looking forward to exploring Lurch! Best regards, Mike 
From: Ken Monks <ken.monks@gm...>  20140518 03:47:27

Hi Craig, Glad to hear you are interested in using Lurch as a learning tool for mathematical proofs. That's exactly what my coauthor and I use it for in our classrooms. Lurch is capable of handling most topics in an Introduction to Proof textbook. The notation and rules might not match your textbook exactly, but some of that can be customized by an advanced Lurch user. We do not yet have a builtin set of rules for real analysis in Lurch, but many of the proofs you will do in the beginning of a typical undergraduate introduction to real analysis course are not proofs in real analysis per se, but rather proofs in logic and elementary set theory, which Lurch does already have builtin. Lurch is completely free software, so there is no harm in downloading it, installing it, and giving it a try. If you have questions feel free to email me offlist at my email address below. Best regards, KEN  Kenneth G. Monks, Ph. D. Professor of Mathematics Department of Mathematics University of Scranton Scranton, PA 18510 Email: monks@...  On Sat, May 17, 2014 at 10:38 PM, Craig Ugoretz <craigugoretz5@...>wrote: > Hello, > > I am starting to delve into amateur mathematics and proofs with a > background in engineering mathematics. I have found an introductory book > on proofs and real analysis that I eventually want to work from. I see > that Lurch has a few defined rules for the real numbers. Are there enough > defined rules for me to use Lurch as a proof checker for real analysis > theorems? I also see that Lurch will be getting more new features with > releases to come. Will Lurch v. 0.8 be OK for my learning purposes, or > should I wait off on this project? > > Sincerely, > Craig > > >  > "Accelerate Dev Cycles with Automated CrossBrowser Testing  For FREE > Instantly run your Selenium tests across 300+ browser/OS combos. > Get unparalleled scalability from the best Selenium testing platform > available > Simple to use. Nothing to install. Get started now for free." > http://p.sf.net/sfu/SauceLabs > _______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss > > 
From: Craig Ugoretz <craigugoretz5@gm...>  20140518 02:38:24

Hello, I am starting to delve into amateur mathematics and proofs with a background in engineering mathematics. I have found an introductory book on proofs and real analysis that I eventually want to work from. I see that Lurch has a few defined rules for the real numbers. Are there enough defined rules for me to use Lurch as a proof checker for real analysis theorems? I also see that Lurch will be getting more new features with releases to come. Will Lurch v. 0.8 be OK for my learning purposes, or should I wait off on this project? Sincerely, Craig 
From: Michael Kohlhase <m.kohlhase@ja...>  20140511 14:54:33

26th OpenMath Workshop Coimbra, Portugal July 7. 2014 colocated with CICM 2014 Submission deadline 7 June http://www.cicmconference.org/2014/openmath/ OBJECTIVES OpenMath (http://www.openmath.org) is a language for exchanging mathematical formulae across applications (such as computer algebra systems). From 2010 its importance has increased in that OpenMath Content Dictionaries were adopted as a foundation of the MathML 3 W3C recommendation (http://www.w3.org/TR/MathML), the standard for mathematical formulae on the Web. Topics we expect to see at the workshop include * Feature Requests (Standard Enhancement Proposals) and Discussions for going beyond OpenMath 2; * Further convergence of OpenMath and MathML 3; * Reasoning with OpenMath; * Software using or processing OpenMath; * OpenMath on the Semantic Web; * New OpenMath Content Dictionaries; Contributions can be either full research papers, Standard Enhancement Proposals, or a description of new Content Dictionaries, particularly ones that are suggested for formal adoption by the OpenMath Society. IMPORTANT DATES (all times are "anywhere on earth") * 7. June 2014: Submission * 20. June 2014: Notification of acceptance or rejection * 5. July 2014: Final revised papers due * 7. July 2014: Workshop (Coimbra time) SUBMISSIONS Submission is via EasyChair (http://www.easychair.org/conferences?conf=om20131). Final papers must conform to the EasyChair LaTeX style. Initial submissions in this format are welcome but not mandatory – but they should be in PDF and within the given limit of pages/words. Submission categories: * Full paper: 5–10 EasyChair pages * Short paper: 1–4 EasyChair pages * CD description: 16 EasyChair pages; a .zip or .tgz file of the CDs must be attached, or a link to the CD provided. * Standard Enhancement Proposal: 110 EasyChair pages (as appropriate w.r.t. the background knowledge required); a .zip or .tgz file of any related implementation (e.g. a Relax NG schema) should be attached. If not in EasyChair format, 500 words count as one page. PROCEEDINGS Electronic proceedings will be published with CEURWS.org. ORGANISATION COMMITTEE * James Davenport (University of Bath, UK) * Michael Kohlhase (Jacobs University Bremen, Germany) PROGRAMME COMMITTEE * James Davenport (University of Bath, UK) * Michael Kohlhase (Jacobs University Bremen, Germany) * Christoph Lange (Rheinische FriedrichWilhelmsUniversität Bonn, Germany) * Lars Hellström (Umeå Universitet, Sweden) * Jan Willem Knopper (Technische Universiteit Eindhoven, Netherlands) * Paul Libbrecht (PH Weingarten) * Chris Rowley (LaTeX3 Project and Open Math Society) Comments/questions/enquiries: to be sent to the organizers 
From: Carter, Nathan <NCARTER@bentley.edu>  20140110 16:52:00

Hello, Lurch email list. This past academic year both of us (Nathan Carter and Ken Monks, collaborators on Lurch) have used the software through large portions of introtoproof courses and gotten very positive results. Of course, the software is far from perfect yet, but our students definitely found it beneficial. We're writing to let you know that we'll both be at the upcoming Joint Mathematics Meetings in Baltimore, MD, and if you want to talk about the possibility of using Lurch in a course like we did, or hear about our experiences, feel free to reply to us offlist and let us know when you're free. (See email addresses below.) We'd be glad to meet facetoface at the JMM or virtually if you're not planning to attend. Finally, Ken will be talking about Lurch at the NSF poster session, 2:154:15pm on Wed 1/15 in Exhibit Hall G, Level 100 BCC. Feel free to stop by there for a more informal question/answer time. Thanks, and hope to see you soon! Nathan Carter Kenneth G. Monks Mathematical Sciences Department Mathematics Department Bentley University University of Scranton ncarter@... ken.monks@... 
From: Christoph LANGE <math.web@gm...>  20131003 11:04:58

Call for Papers for a Special Issue of MATHEMATICS IN COMPUTER SCIENCE ENABLING DOMAIN EXPERTS TO USE FORMALISED REASONING http://www.cs.bham.ac.uk/research/projects/formare/pubs/mcsdoform/ Guest editors: Manfred Kerber, Christoph Lange, Colin Rowat We invite highquality original research papers to a special issue of the Birkhäuser/Springer journal Mathematics in Computer Science on the use of systems based on a formal, explicit, machineverifiable representation of knowledge in application domains such as economics, engineering, health care, education. Examples include: * problems from application domains, which could benefit from better verification and knowledge management facilities, and * knowledge management and verification tools, which domain experts can use without a computer science background. (Read more about our topics of interest) For further examples, please see the Symposium on Enabling Domain Experts to use Formalised Reasoning (http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/) held at the annual convention of the AISB (Society for the Study of Artificial Intelligence and Simulation of Behaviour) in April 2013. Submission: 31 October 2013 Notification: 15 December 2013 Revised version due: 15 January 2014 Final version due: 15 February 2014 Publication (expected): April 2014 Topics of interest include but are not limited to: * for domain experts: what problems in application domains could benefit from better verification and knowledge management facilities? Possible fields include:  Example 1 (economics): auctions, valueatrisk models, trading algorithms, market design  Example 2 (engineering): system interoperability, manufacturing processes, product classification * for computer scientists: how to provide the right knowledge management and verification tools to domain experts without a computer science background?  wikis and blogs for informal, semantic, semiformal, and formal mathematical knowledge;  general techniques and tools for online collaborative mathematics;  tools for collaboratively producing, presenting, publishing, and interacting with online mathematics;  automation and humancomputer interaction aspects of mathematical wikis;  ontologies and knowledge bases designed to support knowledge management and verification in application domains;  practical experiences, usability aspects, feasibility studies;  evaluation of existing tools and experiments;  requirements, user scenarios and goals. Submissions should be approximately 20 pages long, should follow publishers' instructions and should be submitted via EasyChair. Potential contributors may contact the guest editors (doformmcs2014@...) to discuss the suitability of topics and papers.  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. Early registration deadline 23 June; http://cicmconference.org/2013/ → Knowledge and Experience Management, 79 October, Bamberg, Germany. Submission until 1 July; http://minf.unibamberg.de/lwa2013/cfp/fgwm/ → Modular Ontologies (WoMO), 15 September, Corunna, Spain. Submission until 5 July; http://www.iaoa.org/womo/2013.html 
From: Christoph LANGE <math.web@gm...>  20130612 14:22:44

Call for Papers for a Special Issue of MATHEMATICS IN COMPUTER SCIENCE ENABLING DOMAIN EXPERTS TO USE FORMALISED REASONING http://www.cs.bham.ac.uk/research/projects/formare/pubs/mcsdoform/ Guest editors: Manfred Kerber, Christoph Lange, Colin Rowat We invite highquality original research papers to a special issue of the Birkhäuser/Springer journal Mathematics in Computer Science on the use of systems based on a formal, explicit, machineverifiable representation of knowledge in application domains such as economics, engineering, health care, education. Examples include: * problems from application domains, which could benefit from better verification and knowledge management facilities, and * knowledge management and verification tools, which domain experts can use without a computer science background. (Read more about our topics of interest) For further examples, please see the Symposium on Enabling Domain Experts to use Formalised Reasoning (http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/) held at the annual convention of the AISB (Society for the Study of Artificial Intelligence and Simulation of Behaviour) in April 2013. Submission: 31 October 2013 Notification: 15 December 2013 Revised version due: 15 January 2014 Final version due: 15 February 2014 Publication (expected): April 2014 Topics of interest include but are not limited to: * for domain experts: what problems in application domains could benefit from better verification and knowledge management facilities? Possible fields include:  Example 1 (economics): auctions, valueatrisk models, trading algorithms, market design  Example 2 (engineering): system interoperability, manufacturing processes, product classification * for computer scientists: how to provide the right knowledge management and verification tools to domain experts without a computer science background?  wikis and blogs for informal, semantic, semiformal, and formal mathematical knowledge;  general techniques and tools for online collaborative mathematics;  tools for collaboratively producing, presenting, publishing, and interacting with online mathematics;  automation and humancomputer interaction aspects of mathematical wikis;  ontologies and knowledge bases designed to support knowledge management and verification in application domains;  practical experiences, usability aspects, feasibility studies;  evaluation of existing tools and experiments;  requirements, user scenarios and goals. Submissions should be approximately 20 pages long, should follow publishers' instructions and should be submitted via EasyChair. Potential contributors may contact the guest editors (doformmcs2014@...) to discuss the suitability of topics and papers.  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. Early registration deadline 23 June; http://cicmconference.org/2013/ → Knowledge and Experience Management, 79 October, Bamberg, Germany. Submission until 1 July; http://minf.unibamberg.de/lwa2013/cfp/fgwm/ → Modular Ontologies (WoMO), 15 September, Corunna, Spain. Submission until 5 July; http://www.iaoa.org/womo/2013.html 
From: Carter, Nathan <NCARTER@bentley.edu>  20130520 12:02:43

Hi, Christoph. I recently received the OK from my institution to attend this conference, so I will be submitting, as you and I discussed a bit offlist. I'm very much looking forward to attending, sharing about Lurch, and learning what else is presented at the conference. Thank you! Nathan Carter Mathematical Sciences Department Associate Director, Honors Program Bentley University (781) 8913171 http://web.bentley.edu/empl/c/ncarter On May 20, 2013, at 7:10 AM, Christoph LANGE <math.semantic.web@...> wrote: > 25th OpenMath Workshop > Bath, UK > 10 July 2013 > colocated with CICM 2013 > Submission deadline 7 June > > http://www.cicmconference.org/2013/openmath/ > > OBJECTIVES > > OpenMath (http://www.openmath.org) is a language for exchanging > mathematical formulae across applications (such as computer algebra > systems). From 2010 its importance has increased in that OpenMath > Content Dictionaries were adopted as a foundation of the MathML 3 W3C > recommendation (http://www.w3.org/TR/MathML), the standard for > mathematical formulae on the Web. > > Topics we expect to see at the workshop include > > * Feature Requests (Standard Enhancement Proposals) and Discussions > for going beyond OpenMath 2; > * Further convergence of OpenMath and MathML 3; > * Reasoning with OpenMath; > * Software using or processing OpenMath; > * OpenMath on the Semantic Web; > * New OpenMath Content Dictionaries; > > Contributions can be either full research papers, Standard Enhancement > Proposals, or a description of new Content Dictionaries, particularly > ones that are suggested for formal adoption by the OpenMath Society. > > IMPORTANT DATES (all times are "anywhere on earth") > > * 7 June: Submission > * 20 June: Notification of acceptance or rejection > * 5 July: Final revised papers due > * 10 July: Workshop > > SUBMISSIONS > > Submission is via EasyChair > (http://www.easychair.org/conferences?conf=om20131). Final papers > must conform to the EasyChair LaTeX style. Initial submissions in > this format are welcome but not mandatory – but they should be in PDF > and within the given limit of pages/words. > > Submission categories: > > * Full paper: 5–10 EasyChair pages > * Short paper: 1–4 EasyChair pages > * CD description: 16 EasyChair pages; a .zip or .tgz file of the > CDs must be attached, or a link to the CD provided. > * Standard Enhancement Proposal: 110 EasyChair pages (as > appropriate w.r.t. the background knowledge required); a .zip or > .tgz file of any related implementation (e.g. a Relax NG schema) > should be attached. > > If not in EasyChair format, 500 words count as one page. > > PROCEEDINGS > > Electronic proceedings will be published with CEURWS.org. > > ORGANISATION COMMITTEE > > * Christoph Lange (University of Birmingham, UK) > * James Davenport (University of Bath, UK) > * Michael Kohlhase (Jacobs University Bremen, Germany) > > PROGRAMME COMMITTEE > > * Lars Hellström (Umeå Universitet, Sweden) > * Jan Willem Knopper (Technische Universiteit Eindhoven, Netherlands) > * Paul Libbrecht (Center for Educational Research in Mathematics > and Technology, MartinLutherUniversity HalleWittenberg) > (to be completed) > > Comments/questions/enquiries: to be sent to > openmathworkshop@... > >  > 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. > Workinprogress deadline 7 June; http://cicmconference.org/2013/ > → OpenMath Workshop, 10 July, Bath, UK. > Submission deadline 7 June; http://cicmconference.org/2013/openmath/ > >  > AlienVault Unified Security Management (USM) platform delivers complete > security visibility with the essential security capabilities. Easily and > efficiently configure, manage, and operate all of your security controls > from a single console and one unified framework. Download a free trial. > http://p.sf.net/sfu/alienvault_d2d > _______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss 
From: Christoph LANGE <math.web@gm...>  20130520 11:17:46

25th OpenMath Workshop Bath, UK 10 July 2013 colocated with CICM 2013 Submission deadline 7 June http://www.cicmconference.org/2013/openmath/ OBJECTIVES OpenMath (http://www.openmath.org) is a language for exchanging mathematical formulae across applications (such as computer algebra systems). From 2010 its importance has increased in that OpenMath Content Dictionaries were adopted as a foundation of the MathML 3 W3C recommendation (http://www.w3.org/TR/MathML), the standard for mathematical formulae on the Web. Topics we expect to see at the workshop include * Feature Requests (Standard Enhancement Proposals) and Discussions for going beyond OpenMath 2; * Further convergence of OpenMath and MathML 3; * Reasoning with OpenMath; * Software using or processing OpenMath; * OpenMath on the Semantic Web; * New OpenMath Content Dictionaries; Contributions can be either full research papers, Standard Enhancement Proposals, or a description of new Content Dictionaries, particularly ones that are suggested for formal adoption by the OpenMath Society. IMPORTANT DATES (all times are "anywhere on earth") * 7 June: Submission * 20 June: Notification of acceptance or rejection * 5 July: Final revised papers due * 10 July: Workshop SUBMISSIONS Submission is via EasyChair (http://www.easychair.org/conferences?conf=om20131). Final papers must conform to the EasyChair LaTeX style. Initial submissions in this format are welcome but not mandatory – but they should be in PDF and within the given limit of pages/words. Submission categories: * Full paper: 5–10 EasyChair pages * Short paper: 1–4 EasyChair pages * CD description: 16 EasyChair pages; a .zip or .tgz file of the CDs must be attached, or a link to the CD provided. * Standard Enhancement Proposal: 110 EasyChair pages (as appropriate w.r.t. the background knowledge required); a .zip or .tgz file of any related implementation (e.g. a Relax NG schema) should be attached. If not in EasyChair format, 500 words count as one page. PROCEEDINGS Electronic proceedings will be published with CEURWS.org. ORGANISATION COMMITTEE * Christoph Lange (University of Birmingham, UK) * James Davenport (University of Bath, UK) * Michael Kohlhase (Jacobs University Bremen, Germany) PROGRAMME COMMITTEE * Lars Hellström (Umeå Universitet, Sweden) * Jan Willem Knopper (Technische Universiteit Eindhoven, Netherlands) * Paul Libbrecht (Center for Educational Research in Mathematics and Technology, MartinLutherUniversity HalleWittenberg) (to be completed) Comments/questions/enquiries: to be sent to openmathworkshop@...  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. Workinprogress deadline 7 June; http://cicmconference.org/2013/ → OpenMath Workshop, 10 July, Bath, UK. Submission deadline 7 June; http://cicmconference.org/2013/openmath/ 
From: Christoph LANGE <math.web@gm...>  20130419 16:40:59

25th OpenMath Workshop Bath, UK 10 July 2013 colocated with CICM 2013 Submission deadline 7 June http://www.cicmconference.org/2013/cicm.php?event=openmath OBJECTIVES OpenMath (http://www.openmath.org) is a language for exchanging mathematical formulae across applications (such as computer algebra systems). From 2010 its importance has increased in that OpenMath Content Dictionaries were adopted as a foundation of the MathML 3 W3C recommendation (http://www.w3.org/TR/MathML), the standard for mathematical formulae on the Web. Topics we expect to see at the workshop include * Feature Requests (Standard Enhancement Proposals) and Discussions for going beyond OpenMath 2; * Further convergence of OpenMath and MathML 3; * Reasoning with OpenMath; * Software using or processing OpenMath; * OpenMath on the Semantic Web; * New OpenMath Content Dictionaries; Contributions can be either full research papers, Standard Enhancement Proposals, or a description of new Content Dictionaries, particularly ones that are suggested for formal adoption by the OpenMath Society. IMPORTANT DATES (all times are "anywhere on earth") * 7 June: Submission * 20 June: Notification of acceptance or rejection * 5 July: Final revised papers due * 10 July: Workshop SUBMISSIONS Submission is via EasyChair (http://www.easychair.org/conferences?conf=om20131). Final papers must conform to the EasyChair LaTeX style. Initial submissions in this format are welcome but not mandatory – but they should be in PDF and within the given limit of pages/words. Submission categories: * Full paper: 5–10 EasyChair pages * Short paper: 1–4 EasyChair pages * CD description: 16 EasyChair pages; a .zip or .tgz file of the CDs must be attached, or a link to the CD provided. * Standard Enhancement Proposal: 110 EasyChair pages (as appropriate w.r.t. the background knowledge required); a .zip or .tgz file of any related implementation (e.g. a Relax NG schema) should be attached. If not in EasyChair format, 500 words count as one page. PROCEEDINGS Electronic proceedings will be published with CEURWS.org. ORGANISATION COMMITTEE * Christoph Lange (University of Birmingham, UK) * James Davenport (University of Bath, UK) * Michael Kohlhase (Jacobs University Bremen, Germany) Comments/questions/enquiries: to be sent to openmathworkshop@...  Christoph Lange, School of Computer Science, University of Birmingham http://cs.bham.ac.uk/~langec/, Skype duke4701 → Intelligent Computer Mathematics, 7–12 July, Bath, UK. Workinprogress deadline 7 June; http://cicmconference.org/2013/ 
From: Ken Monks <ken.monks@gm...>  20130222 16:20:45

Welcome! I'm glad to hear that you are thinking about using Lurch in your Number Theory course next fall. I am currently teaching and Introduction to Proof course at my university using Lurch, and as part of that course I am developing an very elementary Number Theory library that is intended for students in that course. Since my course is not a fullblown course on Number Theory it will only contain Lurch rules for induction, divisibility, gcd, lcm, primes, composites, and congruence. We do not actually define the natural numbers from axioms (but have some rules for recognizing, integer constants and doing arithmetic with them) since I'm really only doing elementary naive set theory and number theory with the focus being on teaching the students how to write mathematical proofs. If you have only a few additional specific topics you would like to see included I would be happy to include them to customize it to your needs. If you require a more substantial number theory package, perhaps doing an axiomatic construction of the natural numbers along the lines of the Peanoaxioms or constructing the natural numbers in ZFC, I would be happy to work with you to develop it. I have middle school level math education majors (a new certification in Pennsylvania) in my current course, and so far they are handling Lurch and the abstraction of the Intro to Proof course quite well. Let me know what topics and definitions you would like to use in your course and we can best plan how to move forward from there. KEN 
From: Luiz Felipe Martins <luizfelipe.martins@gm...>  20130221 10:37:25

Hi. I just downloaded Lurch and played with it a bit, and I am very impressed. I am definitely considering using it for my Number Theory class in the fall. This is a class mostly for future teachers, that might have little exposure to writing proofs. Anybody out there with a similar experience? Felipe Martins. 
From: Ken Monks <ken.monks@gm...>  20130115 23:41:27

Hi Nick, I investigated it further and I think I know what might be causing this problem. Lurch allows you to change the default font for documents to any font you like. However in the current version the set of unicode math symbols that Lurch provides on the symbol toolbar are only guaranteed to be present in the default document font, DejaVu Sans. As an experiment I just changed my default document font to Times New Roman (on linux) and I can confirm that the phi symbol does not display. So for the time being, if you run into any missing math symbols in your document, try changing them back to DejaVu Sans font and that should fix the problem. I've added this information to our FAQ page. http://lurch.sourceforge.net/faq/ Thanks again for your helpful feedback! KEN On Tue, Jan 15, 2013 at 12:23 PM, Ken Monks <ken.monks@...> wrote: > Hi Nick, > > Thanks for the feedback! > > I just installed lurch on a fresh installation of Xubuntu 12.10, and the > phi symbol you mentioned shows up just fine. So it sounds like there is > something about your particular installation that's messing it up. If you > want to email me directly, perhaps you and I can sort it out. > > KEN > > > On Fri, Jan 11, 2013 at 3:28 PM, Nicu Tofan <nicu.tofan@...> wrote: > >> Hello! >> >> >> On Page 9 of 10: Variable and Constant Declarations of the tutorial the >> following quoted text: >> >> >> "Let ϕ be a constant such that cos(ϕ)=ϕ." >> >> >> in the first paragraph does not print the phi character. I assume is a >> font related problem (using Xubuntu 12.10 ), since changing it (the font >> for this text) will show the proper symbol. >> >> >> Nick >> >> >>  >> Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and >> much more. Get web development skills now with LearnDevNow  >> 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. >> SALE $99.99 this month only  learn more at: >> http://p.sf.net/sfu/learnmore_122812 >> _______________________________________________ >> Lurchdiscuss mailing list >> Lurchdiscuss@... >> https://lists.sourceforge.net/lists/listinfo/lurchdiscuss >> >> > 
From: Carter, Nathan <NCARTER@bentley.edu>  20130115 18:38:24

Good question. There are several small bottlenecks, but the largest one is the patternmatching algorithm used when validating, which compares premises and conclusions to the forms they ought to match. This routine is called a great number of times and is not very fast. Fixing it is this ticket: https://sourceforge.net/apps/trac/lurch/ticket/395 There are several other things that take processing time, and should have their speed improved, but that is the primary one. It's roughly 4x as slow as the nexthighestpriority item. Nathan On Jan 15, 2013, at 1:31 PM, Nicu Tofan <nicu.tofan@...<mailto:nicu.tofan@...>> wrote: By the way, I'm curious about what's the bottleneck in Lurch? Notices is a bit slow when validating and loading. Is it the QTextEditor? (I haven't got the time, yet, to look at Lurch's source code in any length, so my question may be far off). Nick 2013/1/15 Ken Monks <ken.monks@...<mailto:ken.monks@...>> Hi Nick, Thanks for the feedback! I just installed lurch on a fresh installation of Xubuntu 12.10, and the phi symbol you mentioned shows up just fine. So it sounds like there is something about your particular installation that's messing it up. If you want to email me directly, perhaps you and I can sort it out. KEN On Fri, Jan 11, 2013 at 3:28 PM, Nicu Tofan <nicu.tofan@...<mailto:nicu.tofan@...>> wrote: Hello! On Page 9 of 10: Variable and Constant Declarations of the tutorial the following quoted text: "Let ϕ be a constant such that cos(ϕ)=ϕ." in the first paragraph does not print the phi character. I assume is a font related problem (using Xubuntu 12.10 ), since changing it (the font for this text) will show the proper symbol. Nick  Master HTML5, CSS3, ASP.NET<http://asp.net/>;, MVC, AJAX, Knockout.js, Web API and much more. Get web development skills now with LearnDevNow  350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only  learn more at: http://p.sf.net/sfu/learnmore_122812 _______________________________________________ Lurchdiscuss mailing list Lurchdiscuss@...<mailto:Lurchdiscuss@...> https://lists.sourceforge.net/lists/listinfo/lurchdiscuss  Master SQL Server Development, Administration, TSQL, SSAS, SSIS, SSRS and more. Get SQL Server skills now (including 2012) with LearnDevNow  200+ hours of stepbystep video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only  learn more at: http://p.sf.net/sfu/learnmore_122512 _______________________________________________ Lurchdiscuss mailing list Lurchdiscuss@...<mailto:Lurchdiscuss@...> https://lists.sourceforge.net/lists/listinfo/lurchdiscuss  Master SQL Server Development, Administration, TSQL, SSAS, SSIS, SSRS and more. Get SQL Server skills now (including 2012) with LearnDevNow  200+ hours of stepbystep video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only  learn more at: http://p.sf.net/sfu/learnmore_122512_______________________________________________ Lurchdiscuss mailing list Lurchdiscuss@... https://lists.sourceforge.net/lists/listinfo/lurchdiscuss 
From: Nicu Tofan <nicu.tofan@gm...>  20130115 18:31:13

By the way, I'm curious about what's the bottleneck in Lurch? Notices is a bit slow when validating and loading. Is it the QTextEditor? (I haven't got the time, yet, to look at Lurch's source code in any length, so my question may be far off). Nick 2013/1/15 Ken Monks <ken.monks@...> > Hi Nick, > > Thanks for the feedback! > > I just installed lurch on a fresh installation of Xubuntu 12.10, and the > phi symbol you mentioned shows up just fine. So it sounds like there is > something about your particular installation that's messing it up. If you > want to email me directly, perhaps you and I can sort it out. > > KEN > > > On Fri, Jan 11, 2013 at 3:28 PM, Nicu Tofan <nicu.tofan@...> wrote: > >> Hello! >> >> >> On Page 9 of 10: Variable and Constant Declarations of the tutorial the >> following quoted text: >> >> >> "Let ϕ be a constant such that cos(ϕ)=ϕ." >> >> >> in the first paragraph does not print the phi character. I assume is a >> font related problem (using Xubuntu 12.10 ), since changing it (the font >> for this text) will show the proper symbol. >> >> >> Nick >> >> >>  >> Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and >> much more. Get web development skills now with LearnDevNow  >> 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. >> SALE $99.99 this month only  learn more at: >> http://p.sf.net/sfu/learnmore_122812 >> _______________________________________________ >> Lurchdiscuss mailing list >> Lurchdiscuss@... >> https://lists.sourceforge.net/lists/listinfo/lurchdiscuss >> >> > > >  > Master SQL Server Development, Administration, TSQL, SSAS, SSIS, SSRS > and more. Get SQL Server skills now (including 2012) with LearnDevNow  > 200+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122512 > _______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss > > 
From: Ken Monks <ken.monks@gm...>  20130115 17:23:33

Hi Nick, Thanks for the feedback! I just installed lurch on a fresh installation of Xubuntu 12.10, and the phi symbol you mentioned shows up just fine. So it sounds like there is something about your particular installation that's messing it up. If you want to email me directly, perhaps you and I can sort it out. KEN On Fri, Jan 11, 2013 at 3:28 PM, Nicu Tofan <nicu.tofan@...> wrote: > Hello! > > > On Page 9 of 10: Variable and Constant Declarations of the tutorial the > following quoted text: > > > "Let ϕ be a constant such that cos(ϕ)=ϕ." > > > in the first paragraph does not print the phi character. I assume is a > font related problem (using Xubuntu 12.10 ), since changing it (the font > for this text) will show the proper symbol. > > > Nick > > >  > Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and > much more. Get web development skills now with LearnDevNow  > 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122812 > _______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss > > 
From: Nicu Tofan <nicu.tofan@gm...>  20130111 21:01:34

Please do, as I seem to have some problems logging into my sourceforge account. I'm guessing I already have the changes that you mentioned, as i cloned the repository with svn checkout https://lurch.svn.sourceforge.net/svnroot/lurch/Lurch/branches/qtwp ((latest revision) Nick 2013/1/11 Carter, Nathan <NCARTER@...> > > You're doing some great, thorough, testing, thanks! I will go ahead and > file this as a bug report in the Trac system myself, since you've already > written it out so carefully, I can just cut and paste. > > By the way, we are about to release another point release 0.77 this > afternoon which will contain a few tiny bug fixes, but not these, since I > just found out about them now. :) > > On Jan 11, 2013, at 12:17 PM, Nicu Tofan <nicu.tofan@...> > wrote: > > > Hello! > > > > I'm following the tutorial and reached : Page 8 of 10 Basic Validation. > > At the end of the page is introduces the autoupdate of the reference. > However, this is the behaviour that I observe: > > (1) fill in the line numbers > > 1 0<1 > > 2 1<2 > > 3 1<3 > > 4 0<2 by the transitivity rule and lines 1 and 2 > > > > (2) press return after line 1: > > 1 0<1 > > 2 abc > > 3 1<2 > > 4 1<3 > > 5 0<2 by the transitivity rule and lines 1 and 3. > > > > (3) backspace to delete the line 2: > > 1 0<1 > > 2 1<2 > > 3 1<3 > > 4 0<2 by the transitivity rule and lines 1 and 1. > > > > Nick > > >  > > Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and > > much more. Get web development skills now with LearnDevNow  > > 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > > SALE $99.99 this month only  learn more at: > > > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > > Lurchdiscuss mailing list > > Lurchdiscuss@... > > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss > > > >  > Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and > much more. Get web development skills now with LearnDevNow  > 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122812 > _______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss > 
From: Carter, Nathan <NCARTER@bentley.edu>  20130111 20:52:07

You're doing some great, thorough, testing, thanks! I will go ahead and file this as a bug report in the Trac system myself, since you've already written it out so carefully, I can just cut and paste. By the way, we are about to release another point release 0.77 this afternoon which will contain a few tiny bug fixes, but not these, since I just found out about them now. :) On Jan 11, 2013, at 12:17 PM, Nicu Tofan <nicu.tofan@...> wrote: > Hello! > > I'm following the tutorial and reached : Page 8 of 10 Basic Validation. > At the end of the page is introduces the autoupdate of the reference. However, this is the behaviour that I observe: > (1) fill in the line numbers > 1 0<1 > 2 1<2 > 3 1<3 > 4 0<2 by the transitivity rule and lines 1 and 2 > > (2) press return after line 1: > 1 0<1 > 2 abc > 3 1<2 > 4 1<3 > 5 0<2 by the transitivity rule and lines 1 and 3. > > (3) backspace to delete the line 2: > 1 0<1 > 2 1<2 > 3 1<3 > 4 0<2 by the transitivity rule and lines 1 and 1. > > Nick >  > Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and > much more. Get web development skills now with LearnDevNow  > 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss 
From: Nicu Tofan <nicu.tofan@gm...>  20130111 20:48:21

:) thanks for the invite, I'm one web camera short. :)) I will fill the ticket in for this and other small things that I've mailed to the list. Nick PS Great job with this project! Congrats! 2013/1/11 Carter, Nathan <NCARTER@...> > > Hi, Nicu! Thanks for trying it out. By the way, we're at the JMM now, > as you may know, so if you want to talk facetoface, just email me offline > (ncarter@...). > > The sourceforge page for code indicates > svn co https://lurch.svn.sourceforge.net/svnroot/lurch lurch > while the install script for Ubuntu uses > svn checkout $REVISION > https://lurch.svn.sourceforge.net/svnroot/lurch/Lurch/branches/qtwp > > As the code in the trunk does not work, I assume the second one is the > path to current development? > > > The former is a superset of the latter, containing both trunk and > branches. We are currently working with the qtwp branch, and will merge > one day when we have time. The trunk code is ancient. :) > > Also, on the first run, I see that editing the name does not update the > introductory dialog: > > You are Anonymous (edit). > > > Ah, good catch. Would you mind filing a ticket for it on the Trac site? > Thanks for your help and interest! > > https://sourceforge.net/apps/trac/lurch/newticket > > Nathan > > > >  > Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and > much more. Get web development skills now with LearnDevNow  > 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122812 > _______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss > > 