Full metadata record
DC FieldValueLanguage
dc.contributor.author黃思誼zh_TW
dc.contributor.author陳穎平zh_TW
dc.contributor.authorHuang, Szu-Yien_US
dc.contributor.authorChen, Ying-pingen_US
dc.date.accessioned2018-01-24T07:41:01Z-
dc.date.available2018-01-24T07:41:01Z-
dc.date.issued2017en_US
dc.identifier.urihttp://etd.lib.nctu.edu.tw/cdrfb3/record/nctu/#GT070556009en_US
dc.identifier.urihttp://hdl.handle.net/11536/141464-
dc.description.abstractBHK interpretation 與 Curry-Howard isomorphism 建立了邏輯與計算的連結,藉由轉換證明過程為程式使電腦可以驗證形式證明的 Proof Assistant,在過去幾十年有重大的發展。演化式演算法作為一個搜索的策略一直以來都有很好的適應性,並且也可以被用於產生程式,因此在本實驗室之前的研究中已經成功的結合演化式演算法與 Proof Assistant,並取得初步的成果證明了這個架構的可行性。本研究將往提升搜索能力,並且嘗試更進階的定理為目的,增加讓 Proof Generator 與人類互動的機制引導演化式演算法的發展。本篇論文將詳細介紹我們所提出的理論以及演算法的設計,包含了我們證明出來的三個定理實驗結果。zh_TW
dc.description.abstractThe 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.en_US
dc.language.isozh_TWen_US
dc.subject演化計算zh_TW
dc.subject證明助理zh_TW
dc.subject自動定理證明zh_TW
dc.subject人類參與zh_TW
dc.subject證明產生器zh_TW
dc.subjectproof generatoren_US
dc.subjectproof assistanten_US
dc.subjectCoqen_US
dc.subjectevolutionary algorithmen_US
dc.subjectautomatic theorem provingen_US
dc.subjecthuman involvementen_US
dc.title以人類參與的演化式搜索證明數學定理zh_TW
dc.titleProving Theorems by Using Evolutionary Search with Human Involvementen_US
dc.typeThesisen_US
dc.contributor.department資訊科學與工程研究所zh_TW
Appears in Collections:Thesis