Poitín: Distilling Theorems From Conjectures | Zendy

Geoff Hamilton | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Poitín: Distilling Theorems From Conjectures

Author(s) -

Geoff Hamilton

Publication year - 2006

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.11.028

Subject(s) - transformation (genetics) , automated theorem proving , divergence (linguistics) , gas meter prover , conjecture , mathematics , algorithm , computer science , distillation , algebra over a field , discrete mathematics , pure mathematics , mathematical proof , biochemistry , chemistry , linguistics , philosophy , geometry , organic chemistry , gene

In this paper, we describe a new fully automatic theorem prover called Poitín which makes use of a novel transformation algorithm called distillation to prove input conjectures. The input conjectures are defined in a functional language and are transformed using the distillation algorithm. The result of this transformation can be easily inspected to see whether the original conjecture is true. Possible divergence of the transformation algorithm is detected, and this information is used to perform generalizations to ensure termination. We give several examples of the application of the theorem prover, and compare it to related work

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research