1 resultado para Non-normal process
em Department of Computer Science E-Repository - King's College London, Strand, London
Filtro por publicador
- Aberdeen University (3)
- Abertay Research Collections - Abertay University’s repository (1)
- Aberystwyth University Repository - Reino Unido (3)
- Academic Research Repository at Institute of Developing Economies (1)
- Adam Mickiewicz University Repository (1)
- AMS Tesi di Dottorato - Alm@DL - Università di Bologna (3)
- AMS Tesi di Laurea - Alm@DL - Università di Bologna (2)
- Applied Math and Science Education Repository - Washington - USA (1)
- Aquatic Commons (1)
- ArchiMeD - Elektronische Publikationen der Universität Mainz - Alemanha (1)
- Archive of European Integration (8)
- Archivo Digital para la Docencia y la Investigación - Repositorio Institucional de la Universidad del País Vasco (12)
- Aston University Research Archive (11)
- Biblioteca de Teses e Dissertações da USP (1)
- Biblioteca Digital da Produção Intelectual da Universidade de São Paulo (5)
- Biblioteca Digital da Produção Intelectual da Universidade de São Paulo (BDPI/USP) (17)
- Biblioteca Digital de la Universidad Católica Argentina (1)
- Biblioteca Digital de Teses e Dissertações Eletrônicas da UERJ (10)
- BORIS: Bern Open Repository and Information System - Berna - Suiça (7)
- Boston University Digital Common (4)
- Brock University, Canada (10)
- Bulgarian Digital Mathematics Library at IMI-BAS (2)
- CaltechTHESIS (13)
- Cambridge University Engineering Department Publications Database (18)
- CentAUR: Central Archive University of Reading - UK (53)
- Chinese Academy of Sciences Institutional Repositories Grid Portal (70)
- Cochin University of Science & Technology (CUSAT), India (14)
- Collection Of Biostatistics Research Archive (2)
- CORA - Cork Open Research Archive - University College Cork - Ireland (2)
- Dalarna University College Electronic Archive (4)
- Deakin Research Online - Australia (82)
- Department of Computer Science E-Repository - King's College London, Strand, London (1)
- DI-fusion - The institutional repository of Université Libre de Bruxelles (1)
- Digital Commons - Michigan Tech (4)
- Digital Commons @ Winthrop University (1)
- DigitalCommons@The Texas Medical Center (7)
- DRUM (Digital Repository at the University of Maryland) (2)
- Duke University (3)
- eResearch Archive - Queensland Department of Agriculture; Fisheries and Forestry (5)
- Glasgow Theses Service (1)
- Greenwich Academic Literature Archive - UK (5)
- Helda - Digital Repository of University of Helsinki (23)
- Indian Institute of Science - Bangalore - Índia (75)
- Instituto Politécnico de Castelo Branco - Portugal (1)
- Instituto Politécnico do Porto, Portugal (7)
- Lume - Repositório Digital da Universidade Federal do Rio Grande do Sul (2)
- National Center for Biotechnology Information - NCBI (1)
- Plymouth Marine Science Electronic Archive (PlyMSEA) (1)
- QSpace: Queen's University - Canada (1)
- QUB Research Portal - Research Directory and Institutional Repository for Queen's University Belfast (80)
- Queensland University of Technology - ePrints Archive (186)
- ReCiL - Repositório Científico Lusófona - Grupo Lusófona, Portugal (1)
- Repositório Científico do Instituto Politécnico de Lisboa - Portugal (1)
- Repositório digital da Fundação Getúlio Vargas - FGV (7)
- Repositório Digital da UNIVERSIDADE DA MADEIRA - Portugal (1)
- Repositório Institucional da Universidade de Aveiro - Portugal (3)
- Repositorio Institucional de la Universidad de Málaga (1)
- Repositório Institucional UNESP - Universidade Estadual Paulista "Julio de Mesquita Filho" (58)
- Repositorio Institucional Universidad de Medellín (1)
- RUN (Repositório da Universidade Nova de Lisboa) - FCT (Faculdade de Cienecias e Technologia), Universidade Nova de Lisboa (UNL), Portugal (2)
- SAPIENTIA - Universidade do Algarve - Portugal (2)
- Universidad del Rosario, Colombia (9)
- Universidad Politécnica de Madrid (4)
- Universidade de Lisboa - Repositório Aberto (2)
- Universidade Federal do Pará (2)
- Universidade Federal do Rio Grande do Norte (UFRN) (11)
- Universidade Técnica de Lisboa (1)
- Universitat de Girona, Spain (4)
- Universitätsbibliothek Kassel, Universität Kassel, Germany (2)
- Université de Lausanne, Switzerland (18)
- Université de Montréal, Canada (53)
- Université Laval Mémoires et thèses électroniques (1)
- University of Michigan (1)
- University of Queensland eSpace - Australia (4)
- University of Washington (1)
- WestminsterResearch - UK (1)
- Worcester Research and Publications - Worcester Research and Publications - UK (2)
Resumo:
In this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors, our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique to reduce higher-order logic to many-sorted (first-order) logic; 2. the free use of new rules for induction subject to certain conditions; 3. the extensive use of previously programmed (total, recursive) functions; 4. the use of templates to make the reasoning much closer to normal mathematical proofs and 5. a conceptual distinction between the computational type theory (for representing programs)and the logical type theory (for reasoning about programs). As an example of our system we give a constructive proof of the well known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.