ArgoGeoChecker
New version with tactics for coherent logic:
Download tactics |
Examples with tactics |
Integrated theorem provers |
Contact
Some corpora
Examples with tactics of several semi-formal theorem proofs (of different granularity) in Hilbert's axiomatic system. File names indicate the level of details used in the proofs.
Please read README file (here or inside folder).
Download ArgoGeoChecker_tactics
Source code: ArgoGeoChecker_tactics
(last update 17.09.2026.)
Please read README.txt file with all the neccessary instructions and explanations on how to use ArgoGeoChecker and its subdirectories.
The program is constantly improved, updates will be made available in the future.
Old version for direct proof:
Download |
Examples |
Integrated theorem provers |
Contact
Some corpora
Examples of several semi-formal theorem proofs in Hilbert's axiomatic system, and in the axiomatic system E
Download ArgoGeoChecker
Source code: ArgoGeoChecker
(last update 26.05.2018.)
Please read README.txt file with all the neccessary instructions and explanations on how to use ArgoGeoChecker and its subdirectories.
The program is constantly improved, updates will be made available in the future.
Integrated theorem provers
All tools that are used within ArgoGeoChecker are publicly available. The program has integrated resolution theorem provers Vampire and E, and a coherent logic theorem prover ArgoCLP
Contact
ArgoGeoChecker is developed by
Sana Stojanovic Djurdjevic
For more information, please send an email to: sana _at_ matf.bg.ac.rs