## 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 (3) Aug (4) Sep Oct Nov Dec

Showing results of 76

1 2 3 4 > >> (Page 1 of 4)
 Re: [Lurch] Lurch for number theory From: Ken Monks - 2014-08-01 18:12:07 Attachments: Message as HTML 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: > > [ > [a|b]:premise > [q]:constant declaration > [b=q.a]:conclusion > [b∈ Z]:conclusion > ]:if-then 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. a|b 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 traffic lights. I guess this proves I'm a mathematician. > Yes, that was the intent. I had a red-green 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 thumbs-up and thumbs-down icon instead, to help such students. I will look forward to hearing about your students' experiences with Lurch! -KEN 
 Re: [Lurch] Lurch for number theory From: Luiz Felipe Martins - 2014-08-01 16:23:34 Attachments: Message as HTML 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 wrote: > On Fri, Aug 1, 2014 at 6:15 AM, Luiz Felipe 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 type-theoretic 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 > _______________________________________________ > Lurch-discuss mailing list > Lurch-discuss@... > https://lists.sourceforge.net/lists/listinfo/lurch-discuss > 
 Re: [Lurch] Lurch for number theory From: Michael Shulman - 2014-08-01 15:40:09 On Fri, Aug 1, 2014 at 6:15 AM, Luiz Felipe 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 type-theoretic 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 
 [Lurch] Lurch for number theory From: Luiz Felipe Martins - 2014-08-01 13:15:27 Attachments: Message as HTML 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: [ [a|b]:premise [q]:constant declaration [b=q.a]:conclusion [b\in Z]:conclusion ]:if-then 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. a|b 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 credit-hour courses to 3 credit-hours, 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 red-yellow-green markers with traffic lights. I guess this proves I'm a mathematician. 
 Re: [Lurch] Fwd: induction bug? From: Ken Monks - 2014-07-30 19:28:11 Attachments: Message as HTML     div-experiments.lurch
 Re: [Lurch] Fwd: induction bug? From: Luiz Felipe Martins - 2014-07-30 15:27:09 Attachments: Message as HTML     div-experiments.lurch
 Re: [Lurch] Fwd: induction bug? From: Ken Monks - 2014-07-28 02:51:19 Attachments: Message as HTML     image.png     image.png
 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. 

Showing results of 76

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