Monday, February 27, 2012

The Data Structures

While the other members of this project have been working on getting the interface working, I have done some work with how the proofs will be stored in memory. The way each frame of an Existential Graph proof is structured works very well as a tree. Each cut (the negation operator, represented as a circle) can be thought of as a node in this tree, with the variables and other cuts contained inside it being its children. Since each frame is one of these trees, the whole proof can be thought of as a list of trees, which is essentially how it will be stored in memory. By structuring it this way, we have a very intuitive system for storing the proof.

Saturday, February 18, 2012

The Shift Towards Javascript

After much debate we've decided to abandon the Qt interface for an html5 javascript based interface. There were many reasons for moving in this direction, but the main ones dealt with mobile/web-support and faster development time. Qt does have some third-party support for buidling Qt apps on Android, but the interface would have to change to fit the app. Qt itself is a terrific platform with its meta-object system sitting on top of C++ with all the neat things like signals and slots and I would highly recommend checking it out for any future desktop applications.  But, the platform has alot more stuff than we need for this project since it is mainly based on doing graphics on a canvas. We don't require any really complex GUI widgets or anything of that sort, just one big canvas to render things on. Qt has a pretty good scene-graph system exactly for this, but there were many hurdles and loops through jump through just to do simple graphical actions and to interact with the rest of the gui. Development time on this system would have taken a lot longer than using a simpler platform. We also hope to turn this into a multi-user proofing system in the long run, either through the web or through some tablet interface and Qt would not extend easily to meet these needs in the future.

So we decided to go to a javascript based system that could work in any browser. This entails heavy cross-platform support and the multi-user system comes in with ease just by making the application a web app. Although there will be a big performance gap fromt Qt, this system will take much less time to develop and optimize. We also have to create very efficient algorithms and data structures for doing the proof process, but this is just more fun stuff to work on! After much searching and testing of different html5 frameworks and libraries I found one thats super-fast and very stable with a great API. Raphael.js will be the scene graph framework we will by using for the project. It works on both desktop and mobile browsers and is supported more or less across the board due to using SVGs instead of the html5 canvas. After just a couple hours of relearning javascript and picking up Raphael's api I've made a good early base for the proof system!

Tuesday, February 14, 2012

Project Intro

Hi, this is the blog for our project: Peirce Logic
Here's a quick description of what we're doing.

Our idea is to create a cross-platform Existential Graph proof system for doing propositional logic proofs. We were suggested to tackle this type project by Professor Bram van Heuveln. Past attempts at software dealing with Existential Graphs have not proven to be very usable due to poor interface designs. One use for this software is in Introductory Logic classes in order to show other ways of doing proofs apart from traditional methods.

The following is a quick summary of what Existential Graphs are by Bram:
Existential Graphs is an alternate logic proof system created by Charles Saunders Peirce. An interesting feature of Existential Graphs is that the nature of proofs in a subtly different way as compared to traditional systems. In traditional formal logic, a proof is a sequence of statements, that one writes after (or under) each other. However, in Existential Graphs, all of the inference rules of the system require one to either add or remove parts to or from a single graphical notation. Thus, a proof in Existential Graphs is the successive transformation of one graph, representing the given information, to another, representing the inferred information. Indeed, one transforms, rather than rewrites. Crudely put: a proof in Existential Graphs is a movie!