Formally Verified Mathematics.
The article presents information on the current technology and its motivations, some recent advances and the prospects for the future. It set aside hardware and software verification deliberately and refers to Donald MacKenzie's book "Mechanizing Proof: Computing, Risk and Trust16." It is stated tha...
| Publicado en: | Communications of the ACM Vol. 57; no. 4; pp. 66 - 76 |
|---|---|
| Autores principales: | , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Apr2014
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=95347706&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 95347706 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Apr2014 vid: 57 iid: 4 pid: 68 pub: Association for Computing Machinery artinfo: ui: 95347706 10.1145/2591012 ppf: 66 ppct: 10 formats: tig: atl: Formally Verified Mathematics. aug: au: AVIGAD, JERMEY HARRISON, JOHN affil: Professor, Department of Philosophy & Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, PA Principal Engineer, Intel Corporation, Hillsboro, OR su: Technology Technological progress Mechanizing Proof: Computing, Risk & Trust (Book) Jordan curves Prime number theorem MacKenzie, Donald Computer software Computer input-output equipment Mathematics theorems sug: subj: Technology Technological progress Mechanizing Proof: Computing, Risk & Trust (Book) Jordan curves Prime number theorem MacKenzie, Donald Computer software Computer input-output equipment Mathematics theorems ab: The article presents information on the current technology and its motivations, some recent advances and the prospects for the future. It set aside hardware and software verification deliberately and refers to Donald MacKenzie's book "Mechanizing Proof: Computing, Risk and Trust16." It is stated that due to developments in computer science it is possible to achieve formalization in practice. Several important theorems have been verified including the prime number theorem, the Jordan curve theorem, and the Brouwer fixed-point theorem. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2014 holdings: @attributes: islocal: N |
|---|