
==========================================================================
ArgoGeoChecker - System for automated verification of semi-formal proofs
==========================================================================

This directory and its subdirectories contain source code for the system
ArgoGeoChecker

----------------------------------------------------------------------------
Usage: ./ArgoGeoChecker AXIOMATIC_SYSTEM th_NAME_proof.txt

AXIOMATIC_SYSTEM is the location of the axiomatic system that is used (with
all definitions and axioms in one file)

NAME is the name of the theorem that is verified

th_NAME_proof.txt is a semi-formal proof of that theorem, and it must be
located in the folder "theorem_and_proofs"

Folder "theorems_and_proofs" will contain automatically generated final proofs.
Isabelle proof: th_NAME_complete_proof.thy,
Coq proof: th_NAME_complete_proof.v,
English proof: th_NAME_complete_proof.pdf,
Serbian proof: th_NAME_kompletan_dokaz.pdf

Folder "xml_proofs" will contain all XML files of the coherent logic vernacular
that are automatically generated. Translation to the target languages will be
performed with the files from the folder "clvernacular".
There are four subfolders, for each of the target languages:
"isar", "coq", "tex", "srpski_tex"

Initially, folders "theorems_and_proofs", "clvernacular", "axiomatic_system",
"ArgoCLP_files" contain files for Hilbert's axiomatic system!
Before working with Avigad's axiomatic system corresponding subfolders
should be copied from "examples/avigad"

Every time the user changes axiomatic system that he is using, he must
copy corresponing subfolders from "examples".

---------------------------------------------------------------------------
For Hilbert's axiomatic system, there is a shortcut:
./ArgoGeoChecker I th_1_proof.txt (for first group of Hilbert's axioms)
./ArgoGeoChecker II th_18_proof.txt (for first and second group)

For axiomatic system E we can use:
./ArgoGeoChecker axiomatic_system/avigad_axioms.p th_prop1_proof.txt

Results are given in the following format:
./ArgoGeoChecker I th_1_proof.txt
th_1_01.p| vampire|  0.03|  0.13|                     ax_I3a |      0.00||
th_1_02.p| vampire|  0.27|  0.21|         ax_sym_ncol ax_D1a |      0.01||
th_1_03.p|       e|  0.28|  0.12|                     ax_I4a |      0.02||
th_1_04.p| vampire|  0.16|  0.38|                      ax_I6 |      0.00||
Seconds: 6

The name of the auxiliary lemma that is proved; resolution theorem prover
that found the smallest axiom set that the lemma can be proved with;
Vampire time; E time; set of axioms that was found; ArgoCLP time
----------------------------------------------------------------------------

Folder "examples" - with subfolders "hilbert" and "avigad".

We made available two sets of semi-formal theorem proofs:
- one in the Hilbert's axiomatic system,
- second in the axiomatic system E (we use the name "avigad").

Each of those folders contain following folders:

"theorems_and_proofs": folder with proofs in the semi-formal proof format
                       
"clvernacular": folder with CLV files and subfolders for each of the target
		languages ("isar", "coq", "tex", "srpski_tex")
                - DTD and XSLT files for the coherent logic vernacular used for
                  the translation to target languages (Isabelle, Coq, English,
		  and Serbian)
		  (those are the same files that are used in the folder
		  xml_proofs for translation to target languages)
		  - shell scripts for automated validation and translation

"axiomatic_system": folder with axioms and definitions

"ArgoCLP_files": additional files for the ArgoCLP prover
----------------------------------------------------------------------------

"examples": files with semi-formal proofs in Avigad's axiomatic system
            and in Hilbert's axiomatic system, with additional files used for
	    generation of proofs in target languages
	    - subfolders - theorems_and_proofs, axiomatic_system, clvernacular,
	    ArgoCLP_files
	    - (THOSE FOLDERS SHOULD BE COPIED INTO THE APPROPRIATE FOLDERS
	    BEFORE RUNNING THE SYSTEM)

"atp": folder with resolution theorem provers Vampire and E, and
       the coherent logic theorem prover ArgoCLP

"xml_proofs": proofs in the XML form of the coherent logic vernacular.
              Has four subfolders - isar, coq, tex, srpski_tex
	      Initially has the same content as the "clvernacular" folder

"scripts": folder with python and shell scripts used for file manipulation

"preprocessing": folder with some simple C++ programs used for preprocessing
		 of input files

"proving": folder used for automated theorem proving and generation of
	   XML proof scripts. Those proof scripts are copied into the
	   "xml_proofs" folder (into its subdirectories), validated,
	   translatated into target languages and final proofs copied into
	   "theorems_and_proofs" folder



----------------------------------------------------------------------------
Before working with selected axiomatic system, the corresponding subfolders
(from the folder "examples") must be used!!!

In case of changes in the axiomatic system, or semi-formal proof, it is
recomended to delete all previously automatically generated files.
The script "clean.sh" should be used for that.

The list of semi-formal theorem proofs in Hilbert's axiomatic system:
./ArgoGeoChecker I th_1_proof.txt
./ArgoGeoChecker I th_2_proof.txt
./ArgoGeoChecker I th_3_proof.txt
./ArgoGeoChecker I th_4_proof.txt
./ArgoGeoChecker I th_5_proof.txt
./ArgoGeoChecker I th_6_proof.txt
./ArgoGeoChecker II th_7_proof.txt
./ArgoGeoChecker II th_8_proof.txt
./ArgoGeoChecker I th_9_proof.txt
./ArgoGeoChecker I th_10_proof.txt
./ArgoGeoChecker I th_11_proof.txt
./ArgoGeoChecker I th_12_proof.txt
./ArgoGeoChecker I th_13_proof.txt
./ArgoGeoChecker I th_14_proof.txt
./ArgoGeoChecker II th_15_proof.txt
./ArgoGeoChecker II th_16_proof.txt
./ArgoGeoChecker II th_17_proof.txt
./ArgoGeoChecker II th_18_proof.txt

The list of semi-formal theorem proofs in axiomatic system E:

./ArgoGeoChecker axiomatic_system/avigad_axioms.p th_prop1_proof.txt
./ArgoGeoChecker axiomatic_system/avigad_axioms.p th_prop1aux1_proof.txt
./ArgoGeoChecker axiomatic_system/avigad_axioms.p th_prop1aux2_proof.txt
./ArgoGeoChecker axiomatic_system/avigad_axioms.p th_prop2_proof.txt

----------------------------------------------------------------------------
For any further questions send an email to: sana@matf.bg.ac.rs
----------------------------------------------------------------------------
