
==========================================================================
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 using the files from the folder "clvernacular".
There are four subfolders, for each of the target languages:
"isar", "coq", "tex", "srpski_tex"

!!!BEFORE validating semi-formal proofs in the selected axiomatic system, first
the corresponding folders must be copied:
    - The user can use scripts: prep_hilbert.sh and prep_avigad.sh
      to copy folders ("theorems_and_proofs", "clvernacular",
      "axiomatic_system", "ArgoCLP_files")
    - Those folders are located in the "examples" directory

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

Content of the directories:

"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

	    We made available two sets of semi-formal theorem proofs:
	    - subfolder "hilbert" with semi-formal proofs in
	      Hilbert's axiomatic system,
	    - subfolder "avigad" with semi-formal proofs in
	      axiomatic system E.

	    Each of those folders contain following folders:

	    "theorems_and_proofs": folder with semi-formal proofs
                       
            "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 used by the ArgoCLP prover

"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. Scripts prep_hilbert.sh and
prep_avigad.sh can be used for copying subfolders.

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

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