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.

No comments:

Post a Comment