Quantum deduction rules
type: Item
instance of: scholarly article
title: Quantum deduction rules
zbMATH Open document ID: 1173.03045
author: Pavel Pudlák
published in: Annals of Pure and Applied Logic
publication date: 2009-02-19T00:00:00Z
review text: This well-written paper deals with many of the important capabilities and limitations of quantum systems for high-speed theorem-proving for propositional logic. Of course, advances in such areas will likely lead to improvements over classical high-speed (1) communication systems, (2) cryptosystems, and (3) computation systems. The reviewer believes the author is very optimistic to suggest that his interesting results can be extended to predicate logic, in general, without special provisos. The author's results may well extend to first-order predicate logic, but not to higher-order predicate logics, due to the presence of various recursively unsolvable problems; e.g., in second-order axiomatic arithmetic, \(A^2\). The author's main achievement is the elegant extension of the classical concept of the Cook-Reckhow Frege System (CRFS) to a useful quantum analogue of CRFS. Finally, the author poses two challenging problems and a conjecture on the existence of a universal quantum Frege system. The reviewer looks forward to seeing the author's novel methods and approaches applied to many-valued logics and modal logics.
reviewed by: Albert A. Mullin
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 68Q17
Mathematics Subject Classification ID: 81P68
Mathematics Subject Classification ID: 03B22
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03D15
zbMATH DE Number: 5509596
zbMATH Keywords: quantum computation
zbMATH Keywords: proof complexity
zbMATH Keywords: quantum Frege proof systems
zbMATH Keywords: propositional logic
zbMATH Keywords: quantum cryptosystems
MaRDI profile type: Publication
full work available at URL: j.apal.2008.09.017
OpenAlex ID: W2024450183
cites work: Quantum computing and hidden variables
cites work: On Interpolation and Automatization for Frege Systems
cites work: Propositional consistency proofs
cites work: The relative efficiency of propositional proof systems
cites work: Q2706552
cites work: Q4343414
cites work: Q4856172
cites work: Some consequences of cryptographical conjectures for \(S_2^1\) and EF
cites work: EXACT QUANTUM FOURIER TRANSFORMS AND DISCRETE LOGARITHM ALGORITHMS
cites work: Q3522420
cites work: Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
DOI: 10.1016/J.APAL.2008.09.017
description: scientific article; zbMATH DE number 5509596