Search

Your search keyword '"many-one reductions"' showing total 2 results
Start Over Descriptor "many-one reductions" Language english
2 results on '"many-one reductions"'

1. Almost complete sets

Author

Ambos-Spies, Klaus, Merkle, Wolfgang, Reimann, Jan, and Terwijn, Sebastiaan A.

Subjects
*POLYNOMIALS, *THEORY, *MATHEMATICS
Abstract

We show that there is a set that is almost complete but not complete under polynomial-time many-one (p-m) reductions for the class E of sets computable in deterministic time 2lin. Here a set in a complexity class C is almost complete for C under some given reducibility if the class of the problems in C that do not reduce to this set has measure 0 in C in the sense of Lutz''s resource-bounded measure theory. We also show that the almost complete sets for E under polynomial time-bounded length-increasing one–one reductions and truth-table reductions of norm 1 coincide with the almost p-m-complete sets for E. Moreover, we obtain similar results for the class EXP of sets computable in deterministic time 2poly. [Copyright &y& Elsevier]

Published
2003
Full Text
View/download PDF

2. Hilbert's Tenth Problem in Coq

Author

Larchey-Wendling, Dominique, Forster, Yannick, Logic, Proof Theory and Programming (TYPES), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Saarland University [Saarbrücken], Herman Geuvers, and ANR-16-CE91-0002,TICAMORE,Traduction et Découverte des Calculs pour les logiques Modales et dérivées(2016)

Subjects
Mathematics::Dynamical Systems, 000 Computer science, knowledge, general works, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, many-one reductions, Diophantine equations, computability theory, Minsky machines, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, undecidability, type theory, Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Coq, Fractran, Hilbert's tenth problem
Abstract

International audience; We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem-in our case by a Minsky machine-is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer.

Published
2019
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results