Skip to content

README.md

Latest commit

 

History

History
61 lines (44 loc) · 1.52 KB

README.md

File metadata and controls

61 lines (44 loc) · 1.52 KB

ea.prover

Source code and obtained results for "Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants"

Prerequisite

Have Coq installed

Get it from https://coq.inria.fr/

Usage

Get a brief description

python ea.prover.py --help

Conduct the experiments included in paper

python ea.prover.py -i proof/andb_prop.v
python ea.prover.py -i proof/andb_true_elim2.v
python ea.prover.py -i proof/andb_true_intro.v
python ea.prover.py -i proof/ev_minus2.v
python ea.prover.py -i proof/n_1.v
python ea.prover.py -i proof/n_le_k.v
python ea.prover.py -i proof/plus_n_0.v
python ea.prover.py -i proof/silly_prob.v
python ea.prover.py -i proof/solving_by_eapply.v
python ea.prover.py -i proof/SSev_even.v

Results inlucded in paper

  • archive/
    • andb_prop/
    • andb_true_intro/
    • n_1/
    • plus_n_0/
    • solving_by_eapply/
    • andb_true_elim2/
    • ev_minus2/
    • n_le_k/
    • silly_prob/
    • SSev_even/

Use

Please cite

Yang, L.-A., Liu, J.-P., Chen, C.-H., & Chen, Y.-p. (2016). Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants. In Proceedings of 2016 IEEE Congress on Evolutionary Computation (CEC 2016), part of 2016 IEEE World Congress on Computational Intelligence (IEEE WCCI 2016) (pp. 4421–4428). doi: 10.1109/CEC.2016.7744352. (arXiv:1602.07455).