Friday, August 30, 2013

Fall 2013 Proposal

Peirce Logic


Group Members: Bharath Santosh (santob2@rpi.edu), Dimitar Dimitrov (dimitd@rpi.edu), Benjammin Caulfield (caulfb2@rpi.edu), Tim Slowikowski (slowit@rpi.edu), Viktor Rumanuk (Rumanv@rpi.edu), Steven Cropp (cropps@rpi.edu), David Kim(kimd14@rpi.edu), Ian Kerins (ianskerins@gmail.com), Christopher Dower (dowerc@rpi.edu)


Our idea is to continue working on our cross-platform Existential Graph proof system for propositional logic proofs. We were suggested to tackle this type of 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!

We are a returning group to RCOS and we are continuing on the foundation of the project which we laid out over the past three semesters. Last semester we’ve added many features to the interface like a minimap, timeline of proofs, and better element interactions. On the proof engine we’ve added a proof grammar to visual logic translator and an automated theorem prover. A web app also has been setup on Google App Engine to handle users and saving proofs.

This semester we have nine members, so we have divided ourselves into three subgroups.  Each subgroup is assigned a separate topic:  touch controls, webapp backend, and logic engine. The touch controls group will focus on adding the ability of using gesture controls to the interface to allow for it to be used on mobile tablets that will be used in a classroom environment. The webapp backend group will be implementing proof saving, storing, loading, and redesigning the ui styles. The logic engine group will begin adding beta existential graphs to the app. Beta graphs are the equivalent of first order logic for existential graphs. We will also work on loading subproofs within a larger proof.