Please view this Website with Firefox. I apologise for the inconvenience.
INTRODUCTION
PROGRAM SYNOPSIS
Hermetica is a program under development. Its purpose is to ellucidate the ins and outs of logic. For the time being it only functions as a proof checker. This web site is essentialy meant to be an overview of the program in its present state rather than a detailed manual.
HOW TO INSTALL AND RUN THE PROGRAM
Since the program is under development there are no releases. If you want to try it out you have to download it from the program's CVS repository. It can be compiled and installed in Linux with the usual
./configure make make install
commands. Since it is presently in development, it probably makes the most sense to install it locally, so you should probably specify a local directory as an install prefex when you run 'configure'. The program will install an executable file called "hermetica" in the appropriate place. For the time being, in order to start the program, simply run that executable.
HOW TO INSTALL AND RUN THE PROGRAM
After you start the program, you should see a window that looks like this:
Notice that the window has two panes. The top pane is used to enter in proofs, and the bottom pane is used to display syntax errors and status messages. After a proof is entered in the top pane, you can hit the "Check proof" button. If there are syntax errors they will be listed in the bottom pane, and parts of the top pane will be hilighted.
If there are no syntax errors, the program will do a step by step check of the proof, annotating each step as it goes, as well as underlining and hilighting. The annotations appear directly in the proof pane. The underlying idea is to make the program behave somewhat like a human teacher marking a student's work.
Notice that in the proof pane there are a number of symbols that cannot be entered from the keyboard. There are two methods of entering symbols:
Use the symbol button panel
As you are typing, hit the "\" key and a popup text entry will appear right next to the cursor. Continue typing the appropriate symbol input code in the text entry, and an autocompletion drop-down menu will appear beneath the entry. This method is far more efficient than using the symbol panel.
