Proving theorems by using evolutionary search with human involvement

Szu Yi Huang, Ying-Ping Chen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Scopus citations

Abstract

The link between logic and computation has been established by the BHK interpretation and the Curry-Howard isomorphism, based on which proof assistants capable of verifying formal proofs by transforming proofs into programs and by computationally evaluating the programs have been developed for the past few decades. Because evolutionary algorithms are search methods with remarkable feasibility and can be used to automatically generate programs, in our previous proposal, evolutionary algorithms and proof assistants were integrated to create a framework able to automatically prove simple theorems. In the present work, we aim to enhance the search ability of the proof generator such that proofs of slightly advanced, complicated theorems can be generated via evolutionary search with human involvement. This article describes in detail the algorithmic design of the proposed proof generator, how and why humans are involved in the process of proof development, and the test runs, in which proofs as Coq formalization of three theorems, the divisibility rule for 3, the sum of an arithmetic series, and the inequality of arithmetic and geometric means, were successfully generated. The developed source code with the obtained experimental results, including the human created rules and the software generated proofs, are released as open source.

Original languageEnglish
Title of host publication2017 IEEE Congress on Evolutionary Computation, CEC 2017 - Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1495-1502
Number of pages8
ISBN (Electronic)9781509046010
DOIs
StatePublished - 5 Jul 2017
Event2017 IEEE Congress on Evolutionary Computation, CEC 2017 - Donostia-San Sebastian, Spain
Duration: 5 Jun 20178 Jun 2017

Publication series

Name2017 IEEE Congress on Evolutionary Computation, CEC 2017 - Proceedings

Conference

Conference2017 IEEE Congress on Evolutionary Computation, CEC 2017
CountrySpain
CityDonostia-San Sebastian
Period5/06/178/06/17

Keywords

  • Automatic theorem proving
  • Coq
  • Evolutionary algorithm
  • Human involvement
  • Proof assistant
  • Proof generator

Fingerprint Dive into the research topics of 'Proving theorems by using evolutionary search with human involvement'. Together they form a unique fingerprint.

Cite this