Work at SourceForge, help us to make it a better place! We have an immediate need for a Support Technician in our San Francisco or Denver office.

## lurch-discuss — Users and developers talk about Lurch: uses, features, improvements wanted, etc.

You can subscribe to this list here.

 2009 2010 2012 2013 2014 Jan Feb Mar (6) Apr May Jun Jul Aug Sep Oct (4) Nov Dec (6) Jan (5) Feb Mar (2) Apr (4) May Jun Jul Aug (6) Sep (3) Oct Nov Dec Jan Feb Mar Apr May Jun Jul (3) Aug Sep Oct Nov Dec Jan (12) Feb (2) Mar Apr (1) May (2) Jun (1) Jul Aug Sep Oct (1) Nov Dec Jan (1) Feb Mar Apr May (4) Jun (6) Jul Aug Sep Oct Nov Dec

Showing results of 69

1 2 3 > >> (Page 1 of 3)
 Re: [Lurch] Fwd: induction bug? From: Michael Shulman - 2014-06-18 05:02:48 Attachments: Message as HTML     image.png     image.png
 [Lurch] Fwd: induction bug? From: Ken Monks - 2014-06-12 06:15:02 Attachments: Message as HTML     image.png     image.png
 Re: [Lurch] induction bug? From: Michael Shulman - 2014-06-04 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 type-theoretic 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 "real-world" 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 upper-division 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/teaching-logic-with-a-proof-assistant , and I'm very excited by it. I'm in the exploring-options stages for an "introduction to proofs" class that I'll be teaching in Spring 2015. 
 Re: [Lurch] induction bug? From: Ken Monks - 2014-06-03 20:11:24 Attachments: Message as HTML     image.png
 Re: [Lurch] Installing on Ubuntu 12.04 From: Ken Monks - 2014-06-03 18:01:15 Attachments: Message as HTML 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 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/how-can-i-install-qt-5-x-on-12-04-lts > which instructed me to "apt-add-repository ppa:ubuntu-sdk-team/ppa" > and then install "qtdeclarative5-dev". I then had to run "qmake" > rather than "qmake-qt5". > > 3. Cloning the lurch git repository didn't also clone the submodule > qtmathjax and the sub-submodule MathJax. > > 4. I needed to install several additional development packages: > qtscript5-dev, libqt5webkit5-dev, and libsqlite3-dev. > > 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 > qtdeclarative5-dev; 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 > _______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss > 
 [Lurch] induction bug? From: Michael Shulman - 2014-06-02 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. 
 [Lurch] Installing on Ubuntu 12.04 From: Michael Shulman - 2014-05-31 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/how-can-i-install-qt-5-x-on-12-04-lts which instructed me to "apt-add-repository ppa:ubuntu-sdk-team/ppa" and then install "qtdeclarative5-dev". I then had to run "qmake" rather than "qmake-qt5". 3. Cloning the lurch git repository didn't also clone the submodule qtmathjax and the sub-submodule MathJax. 4. I needed to install several additional development packages: qtscript5-dev, libqt5webkit5-dev, and libsqlite3-dev. 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 qtdeclarative5-dev; 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 
 Re: [Lurch] Lurch and real analysis From: Ken Monks - 2014-05-18 03:47:27 Attachments: Message as HTML Hi Craig, Glad to hear you are interested in using Lurch as a learning tool for mathematical proofs. That's exactly what my co-author 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 built-in 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 built-in. 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 off-list 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 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 Cross-Browser 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 > _______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss > > 
 [Lurch] Lurch and real analysis From: Craig Ugoretz - 2014-05-18 02:38:24 Attachments: Message as HTML 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 
 [Lurch] First Call for Papers: 26. OpenMath Workshop (at CICM 2014; July 7. July 2014) From: Michael Kohlhase - 2014-05-11 14:54:33 26th OpenMath Workshop Coimbra, Portugal July 7. 2014 co-located with CICM 2014 Submission deadline 7 June http://www.cicm-conference.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: 1-6 EasyChair pages; a .zip or .tgz file of the CDs must be attached, or a link to the CD provided. * Standard Enhancement Proposal: 1-10 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 CEUR-WS.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 Friedrich-Wilhelms-Universitä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 
 [Lurch] Lurch at the JMM From: Carter, Nathan - 2014-01-10 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 intro-to-proof 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 off-list and let us know when you're free. (See email addresses below.) We'd be glad to meet face-to-face 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:15-4: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@... 
 [Lurch] 2nd CfP (deadline 31 Oct) Math. in Comp. Sci. Special Issue 'Enabling Domain Experts to use Formalised Reasoning' From: Christoph LANGE - 2013-10-03 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/mcs-doform/ Guest editors: Manfred Kerber, Christoph Lange, Colin Rowat We invite high-quality 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, machine-verifiable 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, value-at-risk 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 human-computer 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://cicm-conference.org/2013/ → Knowledge and Experience Management, 7-9 October, Bamberg, Germany. Submission until 1 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/ → Modular Ontologies (WoMO), 15 September, Corunna, Spain. Submission until 5 July; http://www.iaoa.org/womo/2013.html 
 [Lurch] CfP for Math. in Computer Science Special Issue on 'Enabling Domain Experts to use Formalised Reasoning' (deadline 31 Oct) From: Christoph LANGE - 2013-06-12 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/mcs-doform/ Guest editors: Manfred Kerber, Christoph Lange, Colin Rowat We invite high-quality 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, machine-verifiable 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, value-at-risk 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 human-computer 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://cicm-conference.org/2013/ → Knowledge and Experience Management, 7-9 October, Bamberg, Germany. Submission until 1 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/ → Modular Ontologies (WoMO), 15 September, Corunna, Spain. Submission until 5 July; http://www.iaoa.org/womo/2013.html 
 Re: [Lurch] 2nd CfP: OpenMath workshop at CICM (10 July, Bath, UK), submission deadline 7 June From: Carter, Nathan - 2013-05-20 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 off-list. 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) 891-3171 http://web.bentley.edu/empl/c/ncarter On May 20, 2013, at 7:10 AM, Christoph LANGE wrote: > 25th OpenMath Workshop > Bath, UK > 10 July 2013 > co-located with CICM 2013 > Submission deadline 7 June > > http://www.cicm-conference.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: 1-6 EasyChair pages; a .zip or .tgz file of the > CDs must be attached, or a link to the CD provided. > * Standard Enhancement Proposal: 1-10 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 CEUR-WS.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, Martin-Luther-University Halle-Wittenberg) > (to be completed) > > Comments/questions/enquiries: to be sent to > openmath-workshop@... > > -- > 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. > Work-in-progress deadline 7 June; http://cicm-conference.org/2013/ > → OpenMath Workshop, 10 July, Bath, UK. > Submission deadline 7 June; http://cicm-conference.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 > _______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss 
 [Lurch] 2nd CfP: OpenMath workshop at CICM (10 July, Bath, UK), submission deadline 7 June From: Christoph LANGE - 2013-05-20 11:17:46 25th OpenMath Workshop Bath, UK 10 July 2013 co-located with CICM 2013 Submission deadline 7 June http://www.cicm-conference.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: 1-6 EasyChair pages; a .zip or .tgz file of the CDs must be attached, or a link to the CD provided. * Standard Enhancement Proposal: 1-10 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 CEUR-WS.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, Martin-Luther-University Halle-Wittenberg) (to be completed) Comments/questions/enquiries: to be sent to openmath-workshop@... -- 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. Work-in-progress deadline 7 June; http://cicm-conference.org/2013/ → OpenMath Workshop, 10 July, Bath, UK. Submission deadline 7 June; http://cicm-conference.org/2013/openmath/ 
 [Lurch] CfP: OpenMath workshop at CICM (10 July, Bath, UK), submission deadline 7 June From: Christoph LANGE - 2013-04-19 16:40:59 25th OpenMath Workshop Bath, UK 10 July 2013 co-located with CICM 2013 Submission deadline 7 June http://www.cicm-conference.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: 1-6 EasyChair pages; a .zip or .tgz file of the CDs must be attached, or a link to the CD provided. * Standard Enhancement Proposal: 1-10 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 CEUR-WS.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 openmath-workshop@... -- 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. Work-in-progress deadline 7 June; http://cicm-conference.org/2013/ 
 Re: [Lurch] Introduction. From: Ken Monks - 2013-02-22 16:20:45 Attachments: Message as HTML 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 full-blown 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 
 [Lurch] Introduction. From: Luiz Felipe Martins - 2013-02-21 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. 
 Re: [Lurch] Phi character not printed From: Ken Monks - 2013-01-15 23:41:27 Attachments: Message as HTML 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 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 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 step-by-step video tutorials by Microsoft MVPs and experts. >> SALE $99.99 this month only -- learn more at: >> http://p.sf.net/sfu/learnmore_122812 >> _______________________________________________ >> Lurch-discuss mailing list >> Lurch-discuss@... >> https://lists.sourceforge.net/lists/listinfo/lurch-discuss >> >> >   Re: [Lurch] Phi character not printed From: Carter, Nathan - 2013-01-15 18:38:24 Attachments: Message as HTML Good question. There are several small bottlenecks, but the largest one is the pattern-matching 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 next-highest-priority item. Nathan On Jan 15, 2013, at 1:31 PM, 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 > 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 > 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 step-by-step video tutorials by Microsoft MVPs and experts. SALE$99.99 this month only -- learn more at: http://p.sf.net/sfu/learnmore_122812 _______________________________________________ Lurch-discuss mailing list Lurch-discuss@... https://lists.sourceforge.net/lists/listinfo/lurch-discuss ------------------------------------------------------------------------------ Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS and more. Get SQL Server skills now (including 2012) with LearnDevNow - 200+ hours of step-by-step video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only - learn more at: http://p.sf.net/sfu/learnmore_122512 _______________________________________________ Lurch-discuss mailing list Lurch-discuss@... https://lists.sourceforge.net/lists/listinfo/lurch-discuss ------------------------------------------------------------------------------ Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS and more. Get SQL Server skills now (including 2012) with LearnDevNow - 200+ hours of step-by-step video tutorials by Microsoft MVPs and experts. SALE$99.99 this month only - learn more at: http://p.sf.net/sfu/learnmore_122512_______________________________________________ Lurch-discuss mailing list Lurch-discuss@... https://lists.sourceforge.net/lists/listinfo/lurch-discuss 
 Re: [Lurch] Phi character not printed From: Nicu Tofan - 2013-01-15 18:31:13 Attachments: Message as HTML 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 > 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 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 step-by-step video tutorials by Microsoft MVPs and experts. >> SALE $99.99 this month only -- learn more at: >> http://p.sf.net/sfu/learnmore_122812 >> _______________________________________________ >> Lurch-discuss mailing list >> Lurch-discuss@... >> https://lists.sourceforge.net/lists/listinfo/lurch-discuss >> >> > > > ------------------------------------------------------------------------------ > Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS > and more. Get SQL Server skills now (including 2012) with LearnDevNow - > 200+ hours of step-by-step video tutorials by Microsoft MVPs and experts. > SALE$99.99 this month only - learn more at: > http://p.sf.net/sfu/learnmore_122512 > _______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss > > 
 Re: [Lurch] Phi character not printed From: Ken Monks - 2013-01-15 17:23:33 Attachments: Message as HTML 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 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 step-by-step video tutorials by Microsoft MVPs and experts. > SALE $99.99 this month only -- learn more at: > http://p.sf.net/sfu/learnmore_122812 > _______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss > >   Re: [Lurch] Bug in auto-update for numbered list items as premises From: Nicu Tofan - 2013-01-11 21:01:34 Attachments: Message as HTML 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/qt-wp ((latest revision) Nick 2013/1/11 Carter, Nathan > > 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 > wrote: > > > Hello! > > > > I'm following the tutorial and reached : Page 8 of 10 Basic Validation. > > At the end of the page is introduces the auto-update 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 step-by-step video tutorials by Microsoft MVPs and experts. > > SALE$99.99 this month only -- learn more at: > > > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > > Lurch-discuss mailing list > > Lurch-discuss@... > > https://lists.sourceforge.net/lists/listinfo/lurch-discuss > > > > ------------------------------------------------------------------------------ > Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and > much more. Get web development skills now with LearnDevNow - > 350+ hours of step-by-step video tutorials by Microsoft MVPs and experts. > SALE $99.99 this month only -- learn more at: > http://p.sf.net/sfu/learnmore_122812 > _______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss >   Re: [Lurch] Bug in auto-update for numbered list items as premises From: Carter, Nathan - 2013-01-11 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 wrote: > Hello! > > I'm following the tutorial and reached : Page 8 of 10 Basic Validation. > At the end of the page is introduces the auto-update 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 step-by-step video tutorials by Microsoft MVPs and experts. > SALE$99.99 this month only -- learn more at: > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss 
 Re: [Lurch] First experience with Lurch From: Nicu Tofan - 2013-01-11 20:48:21 Attachments: Message as HTML :) 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 > > 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 face-to-face, 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/qt-wp > > 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 qt-wp 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 step-by-step video tutorials by Microsoft MVPs and experts. > SALE$99.99 this month only -- learn more at: > http://p.sf.net/sfu/learnmore_122812 > _______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss > > 

Showing results of 69

1 2 3 > >> (Page 1 of 3)