Skip to content
Source code and obtained results for "Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants"
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
archive
proof
.gitattributes
Definitions.v
LICENSE
README.md
ea.prover.py
library
tactic_base

README.md

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

You can’t perform that action at this time.