Archive for the ‘Mathematical Reasoning’ Category (Sharing Mathematical Text on the Web) [Leading Feds Into Woods of Logicism]

Wednesday, November 1st, 2017

From About is a website meant for sharing snippets of mathematical text with others on the web. This is a pastebin for mathematics. This website was born out of a one night hack on Sunday 25, 2012.

Posting and sharing

A new post can be composed by visiting the home page and writing or pasting code in the box on the left hand pane of the page. Once a post is composed and submitted, the page is saved and it becomes accessible with a new unique URL. The new page looks similar to this page and it has a unique URL of its own. The URL can be shared with anyone on the web and he or she will be able to visit your post.


The post can be composed in a mixture of plain text, LaTeX, Markdown and HTML. HTML tags commonly used for formatting text elements are supported. For a demonstration on how LaTeX is rendered, see the demo page. To quickly get started with posting math, see the tutorial.

Bug reports and suggestions

If you come across any bugs, or if you have any suggestions, please email Susam Pal at or report an issue at

Your mileage will vary but drawing on Principia Mathematica without citation will leave any government agents tracking your posts in the wilds of 20th century logicism. Unlikely they will damage anything.

If your Principia notation skills are weak, consider The Notation in Principia Mathematica to translate proofs into late 20th century logic notation.

Wild Maths – explore, imagine, experiment, create!

Wednesday, November 2nd, 2016

Wild Maths – explore, imagine, experiment, create!

From the webpage:

Mathematics is a creative subject. It involves spotting patterns, making connections, and finding new ways of looking at things. Creative mathematicians play with ideas, draw pictures, have the courage to experiment and ask good questions.

Wild Maths is a collection of mathematical games, activities and stories, encouraging you to think creatively. We’ve picked out some of our favourites below – have a go at anything that catches your eye. If you want to explore games, challenges and investigations linked by some shared mathematical areas, click on the Pathways link in the top menu.

The line:

It involves spotting patterns, making connections, and finding new ways of looking at things.

is true of data science as well.

I’m going to print out Can you traverse it?, to keep myself honest, if nothing else. 😉


Category Theory 1.1

Thursday, August 25th, 2016

Motivation and philosophy.

Bartosz Milewski is the author of the category series: Category Theory for Programmers.


Category theory definition dependencies

Friday, August 5th, 2016

Category theory definition dependencies by John D. Cook.

From the post:

The diagram below shows how category theory definitions build on each other. Based on definitions in The Joy of Cats.


You will need John’s full size image for this to really be useful.

Prints to 8 1/2 x 11 paper.

There’s a test of your understanding of category theory.

Use John’s dependency graph and on (several) separate pages, jot down your understanding of each term.

Intuitionism and Constructive Mathematics 80-518/818 — Spring 2016

Saturday, January 9th, 2016

Intuitionism and Constructive Mathematics 80-518/818 — Spring 2016

From the course description:

In this seminar we shall read primary and secondary sources on the origins and developments of intuitionism and constructive mathematics from Brouwer and the Russian constructivists, Bishop, Martin-Löf, up to and including modern developments such as homotopy type theory. We shall focus both on philosophical and metamathematical aspects. Topics could include the Brouwer-Heyting-Kolmogorov (BHK) interpretation, Kripke semantics, topological semantics, the Curry-Howard correspondence with constructive type theories, constructive set theory, realizability, relations to topos theory, formal topology, meaning explanations, homotopy type theory, and/or additional topics according to the interests of participants.


  • Jean van Heijenoort (1967), From Frege to Gödel: A Source Book in Mathematical Logic 1879–1931, Cambridge, MA: Harvard University Press.
  • Michael Dummett (1977/2000), Elements of Intuitionism (Oxford Logic Guides, 39), Oxford: Clarendon Press, 1977; 2nd edition, 2000.
  • Michael Beeson (1985), Foundations of Constructive Mathematics, Heidelberg: Springer Verlag.
  • Anne Sjerp Troelstra and Dirk van Dalen (1988), Constructivism in Mathematics: An Introduction (two volumes), Amsterdam: North Holland.

Additional resources

Not online but a Spring course at Carnegie Mellon with a reading list that should exercise your mental engines!

Any subject with a two volume “introduction” (Anne Sjerp Troelstra and Dirk van Dalen), is likely to be heavy sledding. 😉

But the immediate relevance to topic maps is evident by this statement from Rosalie Iemhoff:

Intuitionism is a philosophy of mathematics that was introduced by the Dutch mathematician L.E.J. Brouwer (1881–1966). Intuitionism is based on the idea that mathematics is a creation of the mind. The truth of a mathematical statement can only be conceived via a mental construction that proves it to be true, and the communication between mathematicians only serves as a means to create the same mental process in different minds.

I would recast that to say:

Language is a creation of the mind. The truth of a language statement can only be conceived via a mental construction that proves it to be true, and the communication between people only serves as a means to create the same mental process in different minds.

There are those who claim there is some correspondence between language and something they call “reality.” Since no one has experienced “reality” in the absence of language, I prefer to ask: Is X useful for purpose Y? rather than the doubtful metaphysics of “Is X true?”

Think of it as helping get down to what’s really important, what’s in this for you?

BTW, don’t be troubled by anyone who suggests this position removes all limits on discussion. What motivations do you think caused people to adopt the varying positions they have now?

It certainly wasn’t a detached and disinterested search for the truth, whatever people may pretend once they have found the “truth” they are presently defending. The same constraints will persist even if we are truthful with ourselves.

Street-Fighting Mathematics – Free Book – Lesson For Semanticists?

Friday, January 1st, 2016

Street-Fighting Mathematics: The Art of Educated Guessing and Opportunistic Problem Solving by Sanjoy Mahajan.

From the webpage:


In problem solving, as in street fighting, rules are for fools: do whatever works—don’t just stand there! Yet we often fear an unjustified leap even though it may land us on a correct result. Traditional mathematics teaching is largely about solving exactly stated problems exactly, yet life often hands us partly defined problems needing only moderately accurate solutions. This engaging book is an antidote to the rigor mortis brought on by too much mathematical rigor, teaching us how to guess answers without needing a proof or an exact calculation.

In Street-Fighting Mathematics, Sanjoy Mahajan builds, sharpens, and demonstrates tools for educated guessing and down-and-dirty, opportunistic problem solving across diverse fields of knowledge—from mathematics to management. Mahajan describes six tools: dimensional analysis, easy cases, lumping, picture proofs, successive approximation, and reasoning by analogy. Illustrating each tool with numerous examples, he carefully separates the tool—the general principle—from the particular application so that the reader can most easily grasp the tool itself to use on problems of particular interest. Street-Fighting Mathematics grew out of a short course taught by the author at MIT for students ranging from first-year undergraduates to graduate students ready for careers in physics, mathematics, management, electrical engineering, computer science, and biology. They benefited from an approach that avoided rigor and taught them how to use mathematics to solve real problems.

I have just started reading Street-Fighting Mathematics but I wonder if there is a parallel between mathematics and the semantics that everyone talks about capturing from information systems.

Consider this line:

Traditional mathematics teaching is largely about solving exactly stated problems exactly, yet life often hands us partly defined problems needing only moderately accurate solutions.

And re-cast it for semantics:

Traditional semantics (Peirce, FOL, SUMO, RDF) is largely about solving exactly stated problems exactly, yet life often hands us partly defined problems needing only moderately accurate solutions.

What if the semantics we capture and apply are sufficient for your use case? Complete with ROI for that use case.

Is that sufficient?

DataGenetics (blog)

Saturday, December 12th, 2015

DataGenetics (blog) by Nick Berry.

I mentioned Nick’s post Estimating “known unknowns” but his blog merits more than a mention of that one post.

As of today, Nick has 217 posts that touch on topics relevant to data science and have illustrations that make them memorable. You will remember those illustrations for discussions among data scientists, customers and even data science interviewers.

Follow Berry’s posts long enough and you may acquire the skill of illustrating data science ideas and problems in straight-forward prose.

Good luck!

Math, Choices, Power and Fractals

Tuesday, January 6th, 2015

How to Fold a Julia Fractal by Steven Wittens.

From the post:

Mathematics has a dirty little secret. Okay, so maybe it’s not so dirty. But neither is it little. It goes as follows:

Everything in mathematics is a choice.

You’d think otherwise, going through the modern day mathematics curriculum. Each theorem and proof is provided, each formula bundled with convenient exercises to apply it to. A long ladder of subjects is set out before you, and you’re told to climb, climb, climb, with the promise of a payoff at the end. “You’ll need this stuff in real life!”, they say, oblivious to the enormity of this lie, to the fact that most of the educated population walks around with “vague memories of math class and clear memories of hating it.”

Rarely is it made obvious that all of these things are entirely optional—that mathematics is the art of making choices so you can discover what the consequences are. That algebra, calculus, geometry are just words we invented to group the most interesting choices together, to identify the most useful tools that came out of them. The act of mathematics is to play around, to put together ideas and see whether they go well together. Unfortunately that exploration is mostly absent from math class and we are fed pre-packaged, pre-digested math pulp instead.

Even if you are not interested in fractals or mathematics, this is a must read post! The graphics and design of the page have to be seen to be believed. Deeply impressive!

If you are interested in fractals or mathematics, you will be stunned by the presentation in this post.

I am going to study the techniques used on this page. I don’t know if they will work with WordPress but if they don’t, I will create HTML pages and link to them from here. Not all the time but for subjects that would benefit from it.

Steven Strogatz says in the tweet I followed to this page:

This is SO good:… You’ll understand imaginary & complex #’s, waves, Julia and Mandelbrot sets as never before

That is so true.

BTW, did you catch the “secret” of mathematics above?

Everything in mathematics is a choice.

Very important to remember when anyone says: “The data says/shows/proves….”

BS. The data doesn’t say anything. The data plus your choices in mathematics gives X result. Not quite the same thing as “The data says/shows/proves….”

In a data driven world, only the powerless will be unable to challenge both data and the choices applied to it.

Which do you want to be? Powerful or powerless?

Book of Proof

Thursday, December 11th, 2014

Book of Proof by Richard Hammack.

From the webpage:

This book is an introduction to the standard methods of proving mathematical theorems. It has been approved by the American Institute of Mathematics’ Open Textbook Initiative. Also see the Mathematical Association of America Math DL review (of the 1st edition), and the Amazon reviews.

The second edition is identical to the first edition, except some mistakes have been corrected, new exercises have been added, and Chapter 13 has been extended. (The Cantor-Bernstein-Schröeder theorem has been added.) The two editions can be used interchangeably, except for the last few pages of Chapter 13. (But you can download them here.)

Order a copy from Amazon or Barnes & Noble for $13.75 or download a pdf for free here. Click here for a pdf copy of the entire book, or get the chapters individually below.

From the Introduction:

This book will initiate you into an esoteric world. You will learn and apply the methods of thought that mathematicians use to verify theorems, explore mathematical truth and create new mathematical theories. This will prepare you for advanced mathematics courses, for you will be better able to understand proofs, write your own proofs and think critically and inquisitively about mathematics.

For a 300+ page book, almost a steal at Amazon for $13.75. A stocking stuffer for Math/CS types on your holiday list. For yourself, grab the pdf version. 😉

Big data projects are raising the bar for being able to think critically about data and the mathematics that underlie its processing.

Big data is by definition too large for human inspection. So you had better be able to think critically about the nature of the data en masse and the methods to be used to process it.

Or to put it another way, if you don’t understand the impact of the data on processing, or assumptions built into the processing methods, how are you going to evaluate big data results?

Just accept them as ground level truth? Ignore them if they contradict your “gut?” Use a Magic 8-Ball?, a Ouija Board?

I would recommend none of the above and working on your data and math critical evaluation skills.


I first saw this in a tweet by David Higginbotham.

Lance’s Lesson – Gödel Incompleteness

Friday, October 10th, 2014

Lance’s Lesson – Gödel Incompleteness by Lance Fortnow.

The “entertainment” category on YouTube is very flexible since it included this lesson on Gödel Incompleteness. 😉

Lance uses Turing machines to “prove” the first and second incompleteness theorems in under a page of notation.

“How Not to Be Wrong”:…

Sunday, June 8th, 2014

“How Not to Be Wrong”: What the literary world can learn from math by Laura Miller.

From the post:

Jordan Ellenberg’s “How Not to Be Wrong: The Power of Mathematical Thinking” is a miscellaneous romp through the world of quantitative reasoning. You can tell just how modular the book is by the way bits of it have been popping up all over the Web of late, promising to explain such mysteries as why so many handsome men are jerks or why an athlete’s performance always seems to suffer a drop-off after he signs a big contract. This pull-apart quality may sound like a bug, but in fact it’s a feature. It makes “How Not to Be Wrong” a rewarding popular math book for just about anyone.

Ellenberg is a professor of mathematics at the University of Wisconsin-Madison who spent “some part of my early 20s thinking I might want to be a Serious Literary Novelist.” (He even published a novel, “The Grasshopper King.”) He has a popular math column at Slate. So Ellenberg can write, and furthermore he brings a set of references to the subject that will make many a numbers-shy humanities major feel right at home. He explains why B.F. Skinner’s “proof” that Shakespeare was not particularly inclined toward poetic alliteration was incorrect, and he is as likely to refer to Robert Frost and Thomas Pynchon as to such mathematical titans as R.A. Fisher and Francis Galton. He takes the playful, gentle, humorous tone of a writer used to cajoling his readers into believing that they can understand what he’s talking about.

At the same time, those who like to pull out a pencil and a piece of paper and work through a few equations for the fun of it should not be utterly put off by the aforementioned cajoling. Interested in a brush-up on plane geometry, the implications of the Prime Numbers Theorem and Yitang Zhang’s recently announced proof of the “bounded gaps” conjecture about the distribution of primes? Pull up a chair. On the other hand, if any sentence containing the term “log N” makes you go cross-eyed and befuddled, you need only turn a few pages ahead to another chapter, where you can read about how two separate math cartels gamed the Massachusetts state lottery.

Laura’s review will leave you convinced that “Have you read ‘How Not to be Wrong’ by Jordan Ellenberg?” should be on your technical interview checklist.

Or at least you should pull examples from it to use in your technical interviews.

Despite all the hype about “big data,” “web scale,” etc., the nature of coherent thinking has not changed. The sooner you winnow out candidates that thing otherwise the better.

Rings — A Second Primer

Sunday, June 2nd, 2013

Rings — A Second Primer by Jeremy Kun.

From the post:

Last time we defined and gave some examples of rings. Recapping, a ring is a special kind of group with an additional multiplication operation that “plays nicely” with addition. The important thing to remember is that a ring is intended to remind us arithmetic with integers (though not too much: multiplication in a ring need not be commutative). We proved some basic properties, like zero being unique and negation being well-behaved. We gave a quick definition of an integral domain as a place where the only way to multiply two things to get zero is when one of the multiplicands was already zero, and of a Euclidean domain where we can perform nice algorithms like the one for computing the greatest common divisor. Finally, we saw a very important example of the ring of polynomials.

In this post we’ll take a small step upward from looking at low-level features of rings, and start considering how general rings relate to each other. The reader familiar with this blog will notice many similarities between this post and our post on group theory. Indeed, the definitions here will be “motivated” by an attempt to replicate the same kinds of structures we found helpful in group theory (subgroups, homomorphisms, quotients, and kernels). And because rings are also abelian groups, we will play fast and loose with a number of the proofs here by relying on facts we proved in our two-post series on group theory. The ideas assume a decidedly distinct flavor here (mostly in ideals), and in future posts we will see how this affects the computational aspects in more detail.

I have a feeling that Jeremy’s posts are eventually going to lead to a very good tome with a title like: Mathematical Foundations of Programming.

To be used when you want to analyze and/or invent algorithms, not simply use them.

Properties of Morphisms

Friday, May 17th, 2013

Properties of Morphisms by Jeremy Kun.

From the post:

This post is mainly mathematical. We left it out of our introduction to categories for brevity, but we should lay these definitions down and some examples before continuing on to universal properties and doing more computation. The reader should feel free to skip this post and return to it later when the words “isomorphism,” “monomorphism,” and “epimorphism” come up again. Perhaps the most important part of this post is the description of an isomorphism.

Isomorphisms, Monomorphisms, and Epimorphisms

Perhaps the most important paradigm shift in category theory is the focus on morphisms as the main object of study. In particular, category theory stipulates that the only knowledge one can gain about an object is in how it relates to other objects. Indeed, this is true in nearly all fields of mathematics: in groups we consider all isomorphic groups to be the same. In topology, homeomorphic spaces are not distinguished. The list goes on. The only way to do determine if two objects are “the same” is by finding a morphism with special properties. Barry Mazur gives a more colorful explanation by considering the meaning of the number 5 in his essay, “When is one thing equal to some other thing?” The point is that categories, more than existing to be a “foundation” for all mathematics as a formal system (though people are working to make such a formal system), exist primarily to “capture the essence” of mathematical discourse, as Mazur puts it. A category defines objects and morphisms, but literally all of the structure of a category lies in its morphisms. And so we study them.

If you are looking for something challenging to read over the weekend, Jeremy’s latest post on morphisms should fit the bill.

The question of “equality” is easy enough to answer as lexical equivalence in UTF-8, but what if you need something more?

Being mindful that “lexical equivalence in UTF-8” is a highly unreliable form of “equality.”

Jeremy is easing us down the road where such discussions can happen with a great deal of rigor.

New Book Explores the P-NP Problem [Explaining Topic Maps]

Monday, April 1st, 2013

New Book Explores the P-NP Problem by Shar Steed.

From the post:

The Golden Ticket: P, NP, and the Search for the Impossible, written by CCC Council and CRA board member, Lance Fortnow is now available. The inspiration for the book came in 2009 when Fortnow published an article on the P-NP problem for Communications of the ACM. With more than 200,000 downloads, the article is one of the website’s most popular, which signals that this is an issue that people are interested in exploring. The P-NP problem is the most important open problem in computer science because it attempts measure the limits of computation.

The book is written to appeal to readers outside of computer science and shed light on the fact that there are deep computational challenges that computer scientists face. To make it relatable, Fortnow developed the “Golden Ticket” analogy, comparing the P-NP problem to the search for the golden ticket in Charlie and the Chocolate Factory, a story many people can relate to. Fortnow avoids mathematical and technical terminology and even the formal definition of the P-NP problem, and instead uses examples to explain concepts

“My goal was to make the book relatable by telling stories. It is a broad based book that does not require a math or computer science background to understand it.”

Fortnow also credits CRA and CCC for giving him inspiration to write the book.

Fortnow has explained the P-NP problem without using “…mathematical and technical commentary and even the formal definition of the P-NP problem….”

Now, we were talking about how difficult it is to explain topic maps?

Suggest we all read this as a source of inspiration for better (more accessible) explanations and tutorials on topic maps.

(I just downloaded it to the Kindle reader on a VM running on my Ubuntu box. This promises to be a great read!)

Methods of Proof — Induction

Saturday, March 23rd, 2013

Methods of Proof — Induction by Jeremy Kun.

Jeremy covers proof by induction in the final post for his “proof” series.

Induction is used to prove statements about natural numbers (positive integers).

Lars Marius Garshol recently concluded slides on big data with:

  • Vast potential
    • to both big data and machine learning
  • Very difficult to realize that potential
    • requires mathematics, which nobody knows
  • We need to wake up!

Big Data 101 by Lars Marius Garshol.

If you want to step up your game with big data, you will need to master mathematics.

Excel and other software can do mathematics but can’t choose the mathematics to apply.

That requires you.

Methods of Proof — Contradiction

Friday, March 1st, 2013

Methods of Proof — Contradiction by Jeremy Kun.

From the post:

In this post we’ll expand our toolbox of proof techniques by adding the proof by contradiction. We’ll also expand on our knowledge of functions on sets, and tackle our first nontrivial theorem: that there is more than one kind of infinity.

Impossibility and an Example Proof by Contradiction

Many of the most impressive results in all of mathematics are proofs of impossibility. We see these in lots of different fields. In number theory, plenty of numbers cannot be expressed as fractions. In geometry, certain geometric constructions are impossible with a straight-edge and compass. In computing theory, certain programs cannot be written. And in logic even certain mathematical statements can’t be proven or disproven.

In some sense proofs of impossibility are hardest proofs, because it’s unclear to the layman how anyone could prove it’s not possible to do something. Perhaps this is part of human nature, that nothing is too impossible to escape the realm of possibility. But perhaps it’s more surprising that the main line of attack to prove something is impossible is to assume it’s possible, and see what follows as a result. This is precisely the method of proof by contradiction:

Assume the claim you want to prove is false, and deduce that something obviously impossible must happen.

There is a simple and very elegant example that I use to explain this concept to high school students in my guest lectures.

I hope you are following this series of posts but if not, at least read the example Jeremy has for proof by contradiction.

It’s a real treat.

Methods of Proof — Contrapositive

Friday, March 1st, 2013

Methods of Proof — Contrapositive by Jeremy Kun.

From the post:

In this post we’ll cover the second of the “basic four” methods of proof: the contrapositive implication. We will build off our material from last time and start by defining functions on sets.

Functions as Sets

So far we have become comfortable with the definition of a set, but the most common way to use sets is to construct functions between them. As programmers we readily understand the nature of a function, but how can we define one mathematically? It turns out we can do it in terms of sets, but let us recall the desired properties of a function:

  • Every input must have an output.
  • Every input can only correspond to one output (the functions must be deterministic).

Jeremy continues his series on proof techniques.

Required knowledge for reading formal CS papers.

Methods of Proof — Direct Implication

Saturday, February 16th, 2013

Methods of Proof — Direct Implication by Jeremy Kun.

From the post:

I recently posted an exploratory piece on why programmers who are genuinely interested in improving their mathematical skills can quickly lose stamina or be deterred. My argument was essentially that they don’t focus enough on mastering the basic methods of proof before attempting to read research papers that assume such knowledge. Also, there are a number of confusing (but in the end helpful) idiosyncrasies in mathematical culture that are often unexplained. Together these can cause enough confusion to stymie even the most dedicated reader. I have certainly experienced it enough to call the feeling familiar.

Now I’m certainly not trying to assert that all programmers need to learn mathematics to improve their craft, nor that learning mathematics will be helpful to any given programmer. All I claim is that someone who wants to understand why theorems are true, or how to tweak mathematical work to suit their own needs, cannot succeed without a thorough understanding of how these results are developed in the first place. Function definitions and variable declarations may form the scaffolding of a C program while the heart of the program may only be contained in a few critical lines of code. In the same way, the heart of a proof is usually quite small and the rest is scaffolding. One surely cannot understand or tweak a program without understanding the scaffolding, and the same goes for mathematical proofs.

And so we begin this series focusing on methods of proof, and we begin in this post with the simplest such methods. I call them the “basic four,” and they are:

  • Proof by direct implication
  • Proof by contradiction
  • Proof by contrapositive, and
  • Proof by induction.

This post will focus on the first one, while introducing some basic notation we will use in the future posts. Mastering these proof techniques does take some practice, and it helps to have some basic mathematical content with which to practice on. We will choose the content of set theory because it’s the easiest field in terms of definitions, and its syntax is the most widely used in all but the most pure areas of mathematics. Part of the point of this primer is to spend time demystifying notation as well, so we will cover the material at a leisurely (for an experienced mathematician: aggravatingly slow) pace.

Parallel processing, multi-core memory architectures, graphs and the like are a long way from the cookbook stage of programming.

If you want to be on the leading edge, some mathematics are going to be required.

This series can bring you one step closer to mathematical literacy.

I say “can” because whether it will or not, depends upon you.

…no Hitchhiker’s Guide…

Saturday, February 9th, 2013

Why there is no Hitchhiker’s Guide to Mathematics for Programmers by Jeremy Kun.

From the post:

Do you really want to get better at mathematics?

Remember when you first learned how to program? I do. I spent two years experimenting with Java programs on my own in high school. Those two years collectively contain the worst and most embarrassing code I have ever written. My programs absolutely reeked of programming no-nos. Hundred-line functions and even thousand-line classes, magic numbers, unreachable blocks of code, ridiculous code comments, a complete disregard for sensible object orientation, negligence of nearly all logic, and type-coercion that would make your skin crawl. I committed every naive mistake in the book, and for all my obvious shortcomings I considered myself a hot-shot programmer! At leaa st I was learning a lot, and I was a hot-shot programmer in a crowd of high-school students interested in game programming.

Even after my first exposure and my commitment to get a programming degree in college, it was another year before I knew what a stack frame or a register was, two more before I was anywhere near competent with a terminal, three more before I fully appreciated functional programming, and to this day I still have an irrational fear of networking and systems programming (the first time I manually edited the call stack I couldn’t stop shivering with apprehension and disgust at what I was doing).

A must read post if you want to be on the cutting edge of programming.

An XML-Format for Conjectures in Geometry (Work-in-Progress)

Saturday, July 14th, 2012

An XML-Format for Conjectures in Geometry (Work-in-Progress) by Pedro Quaresma.


With a large number of software tools dedicated to the visualisation and/or demonstration of properties of geometric constructions and also with the emerging of repositories of geometric constructions, there is a strong need of linking them, and making them and their corpora, widely usable. A common setting for interoperable interactive geometry was already proposed, the i2g format, but, in this format, the conjectures and proofs counterparts are missing. A common format capable of linking all the tools in the field of geometry is missing. In this paper an extension of the i2g format is proposed, this extension is capable of describing not only the geometric constructions but also the geometric conjectures. The integration of this format into the Web-based GeoThms, TGTP and Web Geometry Laboratory systems is also discussed.

The author notes open questions as:

  • The xml format must be complemented with an extensive set of converters allowing the exchange of information between as many geometric tools as possible.
  • The databases queries, as in TGTP, raise the question of selecting appropriate keywords. A fine grain index and/or an appropriate geometry ontology should be addressed.
  • The i2gatp format does not address proofs. Should we try to create such a format? The GATPs produce proofs in quite different formats, maybe the construction of such unifying format it is not possible and/or desirable in this area.

The “keywords,” “fine grained index,” “geometry ontology,” question yells “topic map” to me.


PS: Converters and different formats also say “topic map,” just not as loudly to me. Your volume may vary. (YVMV)


Mathematical Reasoning Group

Thursday, May 31st, 2012

Mathematical Reasoning Group

From the homepage:

The Mathematical Reasoning Group is a distributed research group based in the Centre for Intelligent Systems and their Applications, a research institute within the School of Informatics at the University of Edinburgh. We are a community of informaticists with interests in theorem proving, program synthesis and artificial intelligence. There is a more detailed overview of the MRG and a list of people. You can also find out how to join the MRG.

I was chasing down proceedings from prior “Large Heterogeneous Data” workshops (damn, that’s a fourth name), when I ran across this jewel as the location of some of the archives.

Has lots of other interesting papers, software, activities.

Sing out if you see something you think needs to appear on this blog.