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 :)

No comments:

Post a Comment