A formalization of multi-tape Turing machines
| Autor: | Andrea Asperti, Wilmer Ricciotti |
|---|---|
| Přispěvatelé: | Asperti, Andrea, Ricciotti, Wilmer |
| Rok vydání: | 2015 |
| Předmět: |
Certified correctne
Theoretical computer science Interactive theorem proving General Computer Science Computational complexity theory Computer science Probabilistic Turing machine Super-recursive algorithm DSPACE computer.software_genre Theoretical Computer Science law.invention Turing machine symbols.namesake Turing completeness Non-deterministic Turing machine law Computer Science::Logic in Computer Science Matita Algorithm characterizations PSPACE Programming language Turing machine examples Universal machine Computer Science (all) Proof assistant NSPACE Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Turing reduction symbols Time hierarchy theorem Universal Turing machine Automatic verification Alternating Turing machine computer |
| Zdroj: | Asperti, A & Ricciotti, W 2015, ' A formalization of multi-tape Turing machines ', Theoretical Computer Science, vol. 603, pp. 23-42 . https://doi.org/10.1016/j.tcs.2015.07.013 |
| ISSN: | 0304-3975 |
| DOI: | 10.1016/j.tcs.2015.07.013 |
| Popis: | We discuss the formalization, in the Matita Theorem Prover, of basic results on multi-tapes Turing machines, up to the existence of a (certified) Universal Machine, and propose it as a natural benchmark for comparing different interactive provers and assessing the state of the art in the mechanization of formal reasoning. The work is meant to be a preliminary step towards the creation of a formal repository in Complexity Theory, and is a small piece in our long-term Reverse Complexity program, aiming to a comfortable, machine independent axiomatization of the field. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect