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!

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:

  • 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.