Skip to content

Latest commit

 

History

History
124 lines (85 loc) · 6.27 KB

README.org

File metadata and controls

124 lines (85 loc) · 6.27 KB
Raw

Examples

We may show a simple example of MATR inferring that (AND alpha (AND beta gamma)) is equivalent to (AND (AND alpha beta) gamma). This example will involve the livecoding setup mentioned previously, though the same example may be achieved using a pre-compiled binary execution of matr.jar, simply omit any steps involving Emacs/Cider.

Requirements

In addition to the AMHR/matr-core repository, we will be using the AMHR/MATRCodelets-REST (MATRCodelets-REST/proof-lite) repository (with the proof-lite branch). For sake of simplicity, we will use the notation <MATRCodelets-REST>/ to refer to the local path of the directory the user has cloned this repository into.

If you don’t have Python 3.x and pip(3) installed, these are also required.
Follow the steps outlined in Livecoding to setup the interactive session. Upon doing so we can start the Codelets server:

$ cd <MATRCodelets-Rest>/
$ pip3 install -r requirements.txt
$ python3 Codelets.py

or

$ cd <MATRCodelets-Rest>/
$ pip install -r requirements.txt
$ python Codelets.py

depending on your default version of Python and pip on your system.

You should see output like the following:

* Serving Flask app "Codelets" (lazy loading)
* Environment: production
  WARNING: Do not use the development server in a production environment.
  Use a production WSGI server instead.
* Debug mode: off
* Running on http://127.0.0.1:5002/ (Press CTRL+C to quit)

We now need to upload a configuration file to MATR. Click on the button that says “Upload config”

A window will pop up allowing you to choose a config file. Click “Click to upload” and navigate to <MATRCodelets-REST>/.

In this directory, select config.yaml, then click “Submit”.

The main box in the center of the page should change from a simple round-cornered rectangle to the same rectangle displayed inside a taller rectangle with the text “ML” written beneath the inner rectangle.

We can then add our axiom (AND alpha (AND beta gamma)). Click the “Add Axiom” button:

A window will appear with a text box allowing you to enter a formula. Enter “(AND alpha (AND beta gamma))” and hit “Submit”.

The formula will show with the s-expression converted to LaTeX

From here now we can add the goal (AND (AND alpha beta) gamma). Click on the button labeled “Add Goal”.

Similar to the “Add Axiom” button, this will open a new window with a text box for you to enter the goal’s formula. Type “(AND (AND alpha beta) gamma)” and hit “Submit”.

The result should be that the rootbox now contains two nodes for the axiom and goal respectively

We can now begin the proof! To do so we select the “Step Proof” button

You will see that MATR has updated the rootbox to show the first step of the proof.

Clicking “Step Proof” again we see the next step of the proof

We at this point see a directed graph from our axiom to our goal. You’ll notice that the top left button is labeled “Switch to full proof”

Clicking this will give the full graph of our proof.

You also will notice that the “Switch to full proof” button changes to a “Switch to min proof” button depending on whether the current proof is in its full or minimum form.

While we’re in the full proof, we may select an arbitrary node and get its proof via the “Get Node’s Proof” button.

Doing so will switch our mouse’s pointer to a crosshair icon. We may then select the node we would like the view the proof of. For example we can view the proof of (AND alpha beta)

To return to the original proof, we can select “Switch to min proof”.

From here we can retrieve a png image of our proof with the “Export Proof to PNG” button.

We can also get the text output of the internal representation of our proof with unrendered latex enclosed by clicking “Proof json with latex”

That’s it! For an animated gif demonstrating some of this process refer to Demonstration

License

Copyright © 2019

This program and the accompanying materials are made available under the terms of the Eclipse Public License 2.0 which is available at http://www.eclipse.org/legal/epl-2.0.

This Source Code may also be made available under the following Secondary Licenses when the conditions for such availability set forth in the Eclipse Public License, v. 2.0 are satisfied: GNU General Public License as published by the Free Software Foundation, either version 2 of the License, or (at your option) any later version, with the GNU Classpath Exception which is available at https://www.gnu.org/software/classpath/license.html.