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}
(3) 
_{Aug}
(4) 
_{Sep}

_{Oct}

_{Nov}

_{Dec}

From: Ken Monks <ken.monks@gm...>  20140801 18:12:07

Hi Felipe, Concerning the definition of "divides". I had not understood the difference > between using an existential expression and introducing a constant in a > rule. What I would like, in the case of divisibility, is to use a rule such > as: > > [ > [ab]:premise > [q]:constant declaration > [b=q.a]:conclusion > [b∈ Z]:conclusion > ]:ifthen rule > > I guess the problem with that is that the constant declaration, when used > as a premise, must immediately precede the conclusion in a proof. Am I > right? > Yes, you are correct. > If so, what is the reason for that? Should something like this work > (assuming divides2 refers to the rule definition above) > > 1. ab given > 2. For some m > 3. b=m.a by divides2 > 4. m∈ Z by divides2, using (1) and (2) > > Is the reason this does not work that constant declarations can't have > labels? If so, why is that? > What we need to prevent is someone using the same constant declaration to be used as a premise for more than one rule. For example, if we didn't have some restriction to prevent that you can imagine student doing things like this: 1. ∃x, x<0 (given) 2. ∃x, x>0 (given) 3. Declare c to be a constant. 4. c<0 by ∃ elimination using (1) and (3) 5. c>0 by ∃ elimination using (2) and (3) 6. c<c by transitivity of < (assuming you've defined this rule) So the restriction that the constant declaration can only be used as a premise for the immediately next line prevents this sort of issue. There are other ways we could have prevented it too, but this was the easiest to implement and seemed the least confusing to explain to the students because it shows that the constant is being declared specifically and only as a consequence of a particular existence statement. That having been said, it would be nice to allow the sort of rule you are suggesting, where there are n conclusions after a constant declaration in the rule, and then allow that declaration to be used as a premise when justifying the next n rules, but that would be quite a bit of work to implement. We will keep it in mind for the next design, however. PS. Only today I noticed the analogy of the redyellowgreen markers with > traffic lights. I guess this proves I'm a mathematician. > Yes, that was the intent. I had a redgreen color blind student in my class last year who could not tell the difference between the red and green icons. So we actually have an option in the Lurch preferences to use a thumbsup and thumbsdown icon instead, to help such students. I will look forward to hearing about your students' experiences with Lurch! KEN 
From: Luiz Felipe Martins <luizfelipe.martins@gm...>  20140801 16:23:34

I never studied type theory, so I guess that's why this approach is not familiar to me. It seems that all depends on the what we want our students to assume. I'd prefer the approach you suggest in general, so if we want we can create (or extend) a rule set to include these. It would not be too hard. That's what I'd do, for example, if I were to teach about fields, for example. I think it would be best, initially, to just create a small specific set of rules instead of importing everything that is available. Then the students could get used to proving things using only the field axioms and the notion of equality. I might do this for number theory. In the beginning of the course, I may use a rule set that just has very basic arithmetic and divisibility. Then I'll add stuff like gcd's, Bezout's theorem, modular arithmetic as needed. It may be a good thing for students to be forced to work in a "restricted" environment, so they can focus exclusively in what has to be proved. I guess I'm gonna call it the "Number Theory Playground", since it is not expected to prove anything line quadratic reciprocity. On Fri, Aug 1, 2014 at 11:39 AM, Michael Shulman <shulman@...> wrote: > On Fri, Aug 1, 2014 at 6:15 AM, Luiz Felipe Martins > <luizfelipe.martins@...> wrote: > > I see now that the "substitute some instances" of a variable is quite > > powerful, and how it is cleverly used in the definition of =. I guess I > was > > approaching it in an axiomatic point of view, where = has to be defined > as > > an equivalence relation. > > Well, in typetheoretic foundations for mathematics, equality *is* > usually defined by reflexivity and substitution, with symmetry and > transitivity proven from those. But even though I'm pretty used to > thinking in type theory now, I generally do consider symmetry and > transitivity to be basic properties in my head, rather than always > applying substitution instead. > > Is there any reason not to include symmetry and transitivity in the > supplied "Equality Rules"? (I'm thinking of them as some of the > "basic lemmas" proven immediately after introducing a definition.) It > might also be convenient to include there something like "if a=b then > A[a/x] = A[b/x]", since proving this from substitution requires an > extra call to reflexivity. One might also generalize this to > multisubstitutions, e.g. "if a=b and c=d then A[a/x,c/y] = > A[b/x,d/y]", which would give a nice way to prove Felipe's example > "x+z=y+t". > > Mike > > >  > Want fast and easy access to all the code in your enterprise? Index and > search up to 200,000 lines of code with a free copy of Black Duck > Code Sight  the same software that powers the world's largest code > search on Ohloh, the Black Duck Open Hub! Try it now. > http://p.sf.net/sfu/bds > _______________________________________________ > Lurchdiscuss mailing list > Lurchdiscuss@... > https://lists.sourceforge.net/lists/listinfo/lurchdiscuss > 
From: Michael Shulman <shulman@sa...>  20140801 15:40:09

On Fri, Aug 1, 2014 at 6:15 AM, Luiz Felipe Martins <luizfelipe.martins@...> wrote: > I see now that the "substitute some instances" of a variable is quite > powerful, and how it is cleverly used in the definition of =. I guess I was > approaching it in an axiomatic point of view, where = has to be defined as > an equivalence relation. Well, in typetheoretic foundations for mathematics, equality *is* usually defined by reflexivity and substitution, with symmetry and transitivity proven from those. But even though I'm pretty used to thinking in type theory now, I generally do consider symmetry and transitivity to be basic properties in my head, rather than always applying substitution instead. Is there any reason not to include symmetry and transitivity in the supplied "Equality Rules"? (I'm thinking of them as some of the "basic lemmas" proven immediately after introducing a definition.) It might also be convenient to include there something like "if a=b then A[a/x] = A[b/x]", since proving this from substitution requires an extra call to reflexivity. One might also generalize this to multisubstitutions, e.g. "if a=b and c=d then A[a/x,c/y] = A[b/x,d/y]", which would give a nice way to prove Felipe's example "x+z=y+t". Mike 
From: Luiz Felipe Martins <luizfelipe.martins@gm...>  20140801 13:15:27

Hi Ken, thanks for the response. Now I see, the approach taken by Lurch is the correct one. Justifying whole proofs instead of each step might actually lead students to write correct proofs without really understanding them completely. We can just say "only yellow and green are allowed in correct proofs". Entering algebra steps as assumptions that are discharged is not that bad. Of course, having some sort of CAS in the background would be nice, but I can see the problem. I guess variables in Lurch (as in logic) are not defined to belong to a "domain". So, when doing proofs in arithmetic modulo an integer, for example, the CAS would happily accept things like division, which is not defined. (It is even more complicated, because division can be defined in some cases, but not in others. I guess one would need s CAS that allows for restricted rule sets, so that we could have different "algebras" for integers, reals, modular arithmetic, matrices, etc. Have you guys considered Sage? For modular arithmetic, for example, it would not be hard to write a Sage module that accepts something from Lurch and checks if it is correct in modular arithmetic. Sage has a JSON interface, so all that is involved is to take expressions as strings and do things like replacing . by *. (There is a caveat. Sage does not work in Windows, so this would have do be done using Sage as a web service, for most users.) I see now that the "substitute some instances" of a variable is quite powerful, and how it is cleverly used in the definition of =. I guess I was approaching it in an axiomatic point of view, where = has to be defined as an equivalence relation. I wonder, however, if some of its uses are too subtle for students, as in the example you gave: 1. x=y 2. z=t 3. x+z=x+z by the reason named 'reflexive' 4. x+z=y+z by 'substitution' of (1) into (3) 5. x+z=y+t by 'substitution' of (2) into (4) (Again I'd avoid this by letting students use "algebra", so it is not a big deal.) Concerning the definition of "divides". I had not understood the difference between using an existential expression and introducing a constant in a rule. What I would like, in the case of divisibility, is to use a rule such as: [ [ab]:premise [q]:constant declaration [b=q.a]:conclusion [b\in Z]:conclusion ]:ifthen rule I guess the problem with that is that the constant declaration, when used as a premise, must immediately precede the conclusion in a proof. Am I right? If so, what is the reason for that? Should something like this work (assuming divides2 refers to the rule definition above) 1. ab given 2. For some m 3. b=m.a by divides2 4. m\in Z by divides2, using (1) and (2) Is the reason this does not work that constant declarations can't have labels? If so, why is that? I am still debating if I can use Lurch for my Number Theory in the Fall. All other things being equal I would give it a try. But my institution is going from a 4 credithour courses to 3 credithours, so all courses had to be shortened by a factor of 3/4, and I am weary of changing too many things at the same time. I might ask a group of students to volunteer to try Lurch this semester to see how they like it. I suspect some would go for it, if I label it as "extra help for writing proofs", and might want to use Lurch to check their work, even if I don't require them to hand in their homework in Lurch. Thanks, Felipe Martins. PS. Only today I noticed the analogy of the redyellowgreen markers with traffic lights. I guess this proves I'm a mathematician. 
From: Ken Monks <ken.monks@gm...>  20140730 19:28:11

From: Luiz Felipe Martins <luizfelipe.martins@gm...>  20140730 15:27:09

From: Ken Monks <ken.monks@gm...>  20140728 02:51:19

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. 