Wednesday, September 25, 2013

String Logic Parsing

As the Peirce Logic team has taken on more members (and with them more ambitious goals), the breadth of topics being covered has really ballooned.  People are now working on touch controls, UI, collision changes, back-end storage, and of course bug fixes aplenty.  But to make sure all this new stuff works and our system remains stable, sometimes old code needs to be re-worked as well.  Enter parsing!  Currently, Peirce Logic can parse a user's logic string and create an object to be drawn as a graph.  Below is a diagram showing roughly the function our parsing provides.

The current code we use for parsing was written by scratch and, while it works perfectly now, it is written in a way that makes adding functionality difficult.  To make sure we have robust and easily modified code, we are writing a new parser using the Open Source tool Peg.js.  Peg.js takes a file specifying a grammar and creates a JavaScript file tailored to parse that specified grammar.  This means that we can keep a short, easy to read, and easy to change grammar file, and swap in the Peg.js generated parser to keep our system up to date and functioning.  Simple!

As a side note, there was some disagreement among operator precedence, some members thought conjunction and disjunction should have equal precedence, but we ended up going with the "standard" we found online, which is as follows:
OperatorPrecedence
¬1
$\wedge$2
$\vee$3
4
$\leftrightarrow$5
Peirce out

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.

Sunday, February 17, 2013

Automated Proof Checking

Define a literal to be either an atomic sentence, or the negation of an atomic sentence. A model is the conjunction of literals so that a literal and its negation are not both in the model.  In existential graphs, a satisfaction graph is the disjunction of models, and looks like this (M_i represents a model):

In satisfaction graphs, you can think of a model as a possible assignment of variables that would make the graph true. It turns out that any existential graph can be converted into a satisfaction graph. If a graph is inconsistent, there can be no possible assignment of values that makes it true (i.e., no models). Therefore, the satisfaction graph for that graph would be an empty cut (or FALSE). Now assume we have two graphs, P and Q, and we'd like to show that Q follows from P. This is the same as saying that the graph conjuncting P and not Q yields a contradiction, and that the satisfaction graph for P and not Q is an empty cut. So, to test if P implies Q, we simply look at the satisfaction graph of P and not Q.

For more info on how to convert a graph into a satisfaction graph, look at:

Sunday, February 10, 2013

Website up!

Peirce Logic is now hosted on google app engine! The process of porting everything to app engine was  painless due to mostly static files for now. Next steps are integrating a user login and then saving proofs into the google app engine data store. There's still a lot to pick up on GAE, but it seems like a great web application deployment service that gives a surprisingly large leeway on its free entry level. Go check it out https://developers.google.com/appengine/!

Sunday, February 3, 2013

Semester 3 Begins

Peirce-Logic has come a long way since its start. Here's a quick overview of what we have working, and what we will try to complete as of this semester:

Done:
• Multiple Selection
• Different Modes (Premise/Insertion/proof)
• All inference rules
• Base web-app

To Do:
• User being able to save proof and load proof
• Hosting with google app engine
• Branching in proof tree
• Store proofs as abstract patterns that can be applied to subsequent proofs
• o   i.e. save a proof as a ‘sequent’ phi -> psi that can be applied to any other proof that has the same pattern phi on an even level (so that it can be transformed into psi) or that has psi on an odd level (in which case psi can be transformed into phi simply by reversing all rules (Erasure from even level becomes Insertion on odd level and vice versa; Double Cut and Iteration/Deiteration are already reversible since they are equivalences)
• o   Relatedly: While you are working on a proof have the ability to focus on (‘lift’) a subgraph and work on just that part, which can later be fit into graph as a whole.
• o   Relatedly: have the ability to work backward (from goal graph to start graph basically)
• Expand/Collapse parts of proof trees (to keep its size more manageable or to hide/emphasis (un)important parts of proof
• Automated theorum proofing
• Server/website: have student log in and instructor log in so student work is secure (and saved on server) but instructor can see work as well
• Various levels of automating. Can be used for many things:
• o   Reordering / resizing of graphs
• o   Simple ‘checking’ of steps
• o   Giving hints
• o   Applying indicated rule where possible
• o   Automated theorem proving (user states that something follows, but system will check)
• o   Automated proof generation (system will create proof or part thereof
• o   Etc.
• Mini-map for zoom
The list is ordered from importance, hopefully we can go through the entire list by the end of the semester.