Introduction

Help

The menu functions on the left-hand side provide the following functionality.

Introduction

Explain what this web site provides and in what context it relates to the e-plato system.

Instructions

Contain instructions on how to create files that are readable by OTTER, the theorem prover used by e-plato in the reasoning.

Create File

Not available yet. You will be able to use a simple editor to edit files to submit to OTTER.

Edit File

Not available yet. You will be able to edit files already uploaded to OTTER.

Delete File

Not available yet. Function to delete already uploaded files.

Upload File

With this option you can upload a text file from your computer to the server where OTTER runs.

Run Otter on File

Use this option to run OTTER on one of the files currently uploaded to the storage directory.The page lists all uploaded files. For each file, there are two available options:

detailed: submits the file to OTTER and provides the maximum level of feedback from the theorem prover.
non-detailed: submits the file to OTTER and if the proof is successful, omits less relevant details, leaving only specific details of the proof itself.

Help

This page.