Monday, December 3, 2012

Late Alpha / Pre-Beta

We have a very basic skeletal system of the whole software, you can currently prove propositional logic using Peirce Logic. We are planning on hosting Peirce Logic soon but until then you can test it from here:

Here is an example of a proof you can solve using Peirce Logic.

Peirce logic starts in Construction mode (indicated by the button in the top right corner of the canvas), in this mode you create the existential graph that you are trying to prove. Remember that everything on a plane is conjuncted(anded) together and a single cut represents a not. Once you finished constructing a proof click on the button in the top right corner to switch in to Proof Mode.

In proof mode there are four possible inference rules:
Erasure can only be done on items that have an even amount of cuts around them. Insertion can only be done in items that have an odd number of cuts around them. Please note currently using insertion makes the system go into insertion mode where you can construct anything in the highlighted cut. Then you must click the insertion mode in the corner to return to the proof mode.

To construct items on the canvas simply double click:
If you make a mistake at any time you can use the back and forward buttons on the right side menu at any time
Start by constructing this proof, then switching to proof mode:

You can select multiple items by holding down Ctrl and clicking two or more items. When you release Ctrl a context menu with options for your selection will appear. For this example select the lower level cut around 'C' with a single cut around then select the higher level cut around 'C' within the second cut around it. On the context menu you will be given the option to deiterate, this will remove the higher level 'C':

Next you can double click the cut around the 'B' and do a reverse double cut to bring the cut with the 'B' to a lower level
Next you can deiterate the cut containing 'B' from the cut containing 'A' and 'B', then double clicking 'A' and reversing the double cut:
Lastly to prove A you simply select the cuts containing 'C' and 'B' and selecting Erasure from the context menu.

Congratulations you have just proved 'A' using the existential graphs :)

Sunday, October 21, 2012

Notorious GUI

        Our recent efforts have been focused on the GUI. A new menu design and many tweaks and fixes for the layout of the interface have been implemented. Currently we are focusing on selection; the ability to do multiple selections is top priority. Our near future plans for the GUI are to finish selection, fix collision between the nodes and bounds of the canvas, adding branching to the timeline, and insertion mode. Insertion mode is in essence a sub canvas to define nodes to be inserted into an existing level on the current proof.

Branching should look something like this on the GUI.

Tuesday, September 25, 2012

Fall 2012

Peirce Logic is back for this fall semester! We are now a two person team of me(Bharath Santosh) and Dimitre Dimitrov. We are building an application to do propsitional logic proofs using a proof system known as existential graphs. More information on this system can be found in our first blog post. All of our system is written in javascript using RaphaelJS and jQuery.

Our initial goals are to finish up main interface for the logic system. This includes work on a menu system, a proof timeline, better interface controls, and a full logic back-end. After work on that is complete we will start shifting the project onto a full web app and setup a system to save proofs on an online database and setup small tutorials for doing these proofs.

Wednesday, April 25, 2012

Github Site Up

We put up the repository using gitub's pages feature:
Go try it out! 

p.s; Send us any bugs you find at santob2 at rpi dot edu!

Thursday, April 19, 2012

Future Plans

The semester is nearing an end but the project will be continuing over the summer and also next semester.
We hope to have the basics of the proof system ready this semester. We've gotten most of the back-end and a large part of the front end working. We still have to get the hardest rule iteration and de-iteration working and also smooth out some of the other rules. After those are set along with a way to switch proof modes and save and load proofs we should be set with the fundamental software. A couple of added touches to the GUI are needed too.

After that there will be a split in the branches of development. Professor Bram van Heuveln is guiding us through the way of adding features to the project for a classroom environment. Some features to be added is multi-user environments, multi-touch environments, logic short-circuiting, and dual-direction proof modes. Since we are doing everything in java-script the multi user feature can easily be integrated from converting this into a full web app. We also hope to eventually port it into a tablet for the multi-touch use. The logic short-circuiting and dual direction proofs are back-end features that will probably be worked on next semester. An automated proof checker will also be added in over the summer or next summer to allow the user to make sure they're on the right track.

Sunday, April 1, 2012

Tree Isomorphism

One interesting problem that has come up recently in this project is to create an algorithm that can efficiently tell if two existential graphs are identical. At first, this sounds like simple tree isomorphism, for which linear time algorithms exist, but its actually more complex then that, since tree isomorphism only compares the structure of the graph, and doesn't check if the variables match up properly. If the graph is highly symmetric, there could be a large number(exponential) of ways that the structure of the graph can be matched, which all have to be checked to make sure the variables match up. This would lead to a very expensive algorithm. Fortunately, we have come up with a efficient (n^2 time) algorithm, which is as follows:

  1. Go through a tree and make a list of all unique variables used in that tree
  2. Make sure that the list is identical to the one for the other tree, otherwise they can't match
  3. Assign each variable in the list a number starting from 2
  4. Go through each tree again, and for every node:
    • If variable n is a child of that node, create a new child node that has n children
    • If the node was empty (no variables or children) create a child node that has one child
  5. Run a tree isomorphism algorithm on the new trees, if they match, then the original graphs were identical

Thursday, March 22, 2012

Proof history

We've implemented tree history functions to store past states of the proof. In existential graphs this is essential because the proof is the series of steps and not contained in any particular state. We've also implemented the first few rules of inference but we haven't connected all of them to the interface yet.

We still need to come up with a method for selecting objects before we can tie some of the rules of inference we've implemented into the interface. We also need to come up with a method for handing insertion of complex structures. I'd prefer to be able to do that without having to use a dialog box or similar.

Currently our proof history system saves the entire tree but we are considering making the history store just the changes instead.

Friday, March 9, 2012

Neat Javascript Graphics Libraries

Here are some really neat javascript libraries if you want to do wonderful graphical things in your browser:

  • CakeJs - This scene-graph library was one of the fastest and most responsive that I found and it has some support for mobile devices too. It has many performance optimizations that are key for using the html5 canvas.
  • Processing.js - The classic Processing graphics framework ported to javascript. The neat thing is that it translates a converts a regular Processing .pde file into a javascript file for use on the canvas. This means you could have a program that works on both a java applet and one that works on an html5 canvas! Plus it has a large community from the javascript side and the enormous processing community.
  • Three.js - A really awesome and powerful library for doing 3D graphics using the canvas or webgl.
  • EaselJS - Another neat scene-graph library, although not as fast as CakeJs it has a lot of support for use with external libraries like animation and sound.
  • Paper.js - A very very very pretty canvas scene-graph library that uses scalable vector graphics(SVGs) to render really clean and fast interactive graphics.
  • Raphael - The library we're using for our project. Its another very very very pretty scene-graph library except it doesn't use the canvas and renders everything directly using SVGs so its externally fast for things with a low load of dynamic and moving content. It also works very fast on mobile devices and supports multi-touch. Also if you've seen the really neat graphs and charts on github, those are similar to what can be done using Raphael.

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!