Search

The development of logic has largely been through the 'deductive' paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual 'reductive' perspective: collections of sufficient premisses are generated from putative conclusions. We call this paradigm, 'reductive logic'. This expression of logic encompass as diverse reasoning activities as proving a formula in a formal system to seeking to meet a friend before noon on Saturday. This paper is a semantical analysis of reductive logic. In particular, we provide mathematical foundations for representing and reasoning about 'reduction operators'. Heuristically, reduction operators may be thought of as `backwards' inference rules. In this paper, we address their mathematical representation, how they are used in the context of reductive reasoning, and, crucially, what makes them 'valid'.

Sandqvist gave a proof-theoretic semantics (P-tS) for classical logic (CL) that explicates the meaning of the connectives without assuming bivalance. Later, he gave a semantics for intuitionistic propositional logic (IPL). While soundness in both cases is proved through standard techniques, the proof completeness for CL is complex and somewhat obscure, but clear and simple for IPL. Makinson gave a simplified proof of completeness for classical propositional logic (CPL) by directly relating the the P-tS to the logic's extant truth-functional semantics. In this paper, we give an elementary, constructive, and native -- in the sense that it does not presuppose the model-theoretic interpretation of classical logic -- proof of completeness the P-tS of CL using the techniques applies for IPL. Simultaneously, we give a proof of soundness and completeness for first-order intuitionistic logic (IL).

A fundamental problem in quantum many-body physics is that of finding ground states of local Hamiltonians. A number of recent works gave provably efficient machine learning (ML) algorithms for learning ground states. Specifically, [Huang et al. Science 2022], introduced an approach for learning properties of the ground state of an $n$-qubit gapped local Hamiltonian $H$ from only $n^{\mathcal{O}(1)}$ data points sampled from Hamiltonians in the same phase of matter. This was subsequently improved by [Lewis et al. Nature Communications 2024], to $\mathcal{O}(\log n)$ samples when the geometry of the $n$-qubit system is known. In this work, we introduce two approaches that achieve a constant sample complexity, independent of system size $n$, for learning ground state properties. Our first algorithm consists of a simple modification of the ML model used by Lewis et al. and applies to a property of interest known beforehand. Our second algorithm, which applies even if a description of the property is not known, is a deep neural network model. While empirical results showing the performance of neural networks have been demonstrated, to our knowledge, this is the first rigorous sample complexity bound on a neural network model for predicting ground state properties. We also perform numerical experiments that confirm the improved scaling of our approach compared to earlier results., Comment: 11 pages, 7 figures + 40-page appendix

A proof of quantumness is an efficiently verifiable interactive test that an efficient quantum computer can pass, but all efficient classical computers cannot (under some cryptographic assumption). Such protocols play a crucial role in the certification of quantum devices. Existing single-round protocols (like asking the quantum computer to factor a large number) require large quantum circuits, whereas multi-round ones use smaller circuits but require experimentally challenging mid-circuit measurements. As such, current proofs of quantumness are out of reach for near-term devices. In this work, we construct efficient single-round proofs of quantumness based on existing knowledge assumptions. While knowledge assumptions have not been previously considered in this context, we show that they provide a natural basis for separating classical and quantum computation. Specifically, we show that multi-round protocols based on Decisional Diffie-Hellman (DDH) or Learning With Errors (LWE) can be "compiled" into single-round protocols using a knowledge-of-exponent assumption or knowledge-of-lattice-point assumption, respectively. We also prove an adaptive hardcore-bit statement for a family of claw-free functions based on DDH, which might be of independent interest. Previous approaches to constructing single-round protocols relied on the random oracle model and thus incurred the overhead associated with instantiating the oracle with a cryptographic hash function. In contrast, our protocols have the same resource requirements as their multi-round counterparts without necessitating mid-circuit measurements, making them, arguably, the most efficient single-round proofs of quantumness to date. Our work also helps in understanding the interplay between black-box/white-box reductions and cryptographic assumptions in the design of proofs of quantumness., Comment: 51 pages

A central concept within informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a 'resource semantics' of the logic. This paper shows how 'inferentialism' -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components., Comment: An abstract of conference paper 'Inferentialist Resource Semantics' (Accepted at MFPS 2024) that was presented at SLSS 2024. arXiv admin note: substantial text overlap with arXiv:2402.09217

Viewing group cohomology as a so-called cohomological functor, G. Mislin has generalised Tate cohomology from finite groups to all discrete groups by defining a completion for cohomological functors in [24]. For any cohomological functor $T^{\bullet}: \mathcal{C} \rightarrow \mathcal{D}$ we have constructed its Mislin completion $\widehat{T}^{\bullet}: \mathcal{C} \rightarrow \mathcal{D}$ in [15] under mild assumptions on the abelian categories $\mathcal{C}$ and $\mathcal{D}$ which generalises Tate cohomology to all $T1$ topological groups. In this paper we investigate the properties of Mislin completions. As their main feature, Mislin completions of Ext-functors detect finite projective dimension of objects in the domain category. We establish a version of dimension shifting, an Eckmann-Shapiro result as well as cohomology products such as external products, cup products and Yoneda products., Comment: 43 pages

A short essay presenting the State-Effect Interpretation of natural deduction rules as an explanatory framework for recent developments in proof-theoretic semantics., Comment: Submitted to 'Logic and Philosophy: Historical and Contemporary Issues Conference'

In systems modelling, a 'system' typically comprises located resources relative to which processes execute. One important use of logic in informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a 'resource semantics' of the logic. This paper shows how inferentialism -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components.

The detection and classification of diseases in Robusta coffee leaves are essential to ensure that plants are healthy and the crop yield is kept high. However, this job requires extensive botanical knowledge and much wasted time. Therefore, this task and others similar to it have been extensively researched subjects in image classification. Regarding leaf disease classification, most approaches have used the more popular PlantVillage dataset while completely disregarding other datasets, like the Robusta Coffee Leaf (RoCoLe) dataset. As the RoCoLe dataset is imbalanced and does not have many samples, fine-tuning of pre-trained models and multiple augmentation techniques need to be used. The current paper uses the RoCoLe dataset and approaches based on deep learning for classifying coffee leaf diseases from images, incorporating the pix2pix model for segmentation and cycle-generative adversarial network (CycleGAN) for augmentation. Our study demonstrates the effectiveness of Transformer-based models, online augmentations, and CycleGAN augmentation in improving leaf disease classification. While synthetic data has limitations, it complements real data, enhancing model performance. These findings contribute to developing robust techniques for plant disease detection and classification., Comment: Accepted by ICAART 2024

The logic of bunched implications (BI) can be seen as the free combination of intuitionistic propositional logic (IPL) and intuitionistic multiplicative linear logic (IMLL). We present here a base-extension semantics (B-eS) for BI in the spirit of Sandqvist's B-eS for IPL, deferring an analysis of proof-theoretic validity, in the sense of Dummett and Prawitz, to another occasion. Essential to BI's formulation in proof-theoretic terms is the concept of a `bunch' of hypotheses that is familiar from relevance logic. Bunches amount to trees whose internal vertices are labelled with either the IMLL context-former or the IPL context-former and whose leaves are labelled with propositions or units for the context-formers. This structure presents significant technical challenges in setting up a base-extension semantics for BI. Our approach starts from the B-eS for IPL and the B-eS for IMLL and provides a systematic combination. Such a combination requires that base rules carry bunched structure, and so requires a more complex notion of derivability in a base and a correspondingly richer notion of support in a base. One reason why BI is a substructural logic of interest is that the `resource interpretation' of its semantics, given in terms of sharing and separation and which gives rise to Separation Logic in the field of program verification, is quite distinct from the `number-of-uses' reading of the propositions of linear logic as resources. This resource reading of BI provides useful intuitions in the formulation of its proof-theoretic semantics. We discuss a simple example of the use of the given B-eS in security modelling.

We have previously found experimental evidence for several quantum phenomena in oxygen-ion implanted of hydrogenated graphite: ferromagnetism, antiferromagnetism, paramagentism, triplet superconductivity, Andreev states, Little-Parks oscillations, Lamb shift, Casimir effect, colossal magnetoresistance, and topologically-protected flat-energy bands [1-6]. Triplet superconductivity results in the formation of Josephson junctions, thus with potential of being used for spintronics applications in the critical area of quantum computing. In this paper, we are showing new experimental evidence for the formation of two-dimensional (2D) spin waves in oxygen-ion enriched and in hydrogenated highly oriented pyrolytic graphite. The temperature evolution of the remanent magnetization Mrem(T) data confirms the formation of spin waves that follow the 2D Heisenberg model with a weak uniaxial anisotropy. In addition, the step-like features also found in the temperature dependence of the electrical resistivity between insulating and metallic states suggest several outstanding possibilities, such as a structural transition, triplet superconductivity, and chiral properties., Comment: 8 pages,7 figures, accepted by the Conference Editors for the CEC-ICMC 2023 Conference for publication in the IOP Conference Series: Materials Science and Engineering, Advances in Cryogenic Engineering

We describe a quantum algorithm for finding the smallest eigenvalue of a Hermitian matrix. This algorithm combines Quantum Phase Estimation and Quantum Amplitude Estimation to achieve a quadratic speedup with respect to the best classical algorithm in terms of matrix dimensionality, i.e., $\widetilde{\mathcal{O}}(\sqrt{N}/\epsilon)$ black-box queries to an oracle encoding the matrix, where $N$ is the matrix dimension and $\epsilon$ is the desired precision. In contrast, the best classical algorithm for the same task requires $\Omega(N)\text{polylog}(1/\epsilon)$ queries. In addition, this algorithm allows the user to select any constant success probability. We also provide a similar algorithm with the same runtime that allows us to prepare a quantum state lying mostly in the matrix's low-energy subspace. We implement simulations of both algorithms and demonstrate their application to problems in quantum chemistry and materials science., Comment: 17 pages, 6 figures, all comments are welcome, additional references added

We characterize planar graphs and graph minors among other graph theoretic notions in terms of right-angled Artin groups (RAAGs). For this, we determine all sets of elements in RAAGs with ears as underlying graphs that are exactly the sets of vertex generators. Generalizing ear decompositions of graphs to loose ear decompositions, we characterize both decompositions in terms of RAAGs. The desired results follow as applications of loose ear decompositions of RAAGs., Comment: Accepted in the "International Journal of Algebra and Computation"

This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL). The starting point is a review of Sandqvist's B-eS for intuitionistic propositional logic (IPL), for which we propose an alternative treatment of conjunction that takes the form of the generalized elimination rule for the connective. The resulting semantics is shown to be sound and complete. This motivates our main contribution, a B-eS for IMLL, in which the definitions of the logical constants all take the form of their elimination rule and for which soundness and completeness are established.

A test of quantumness is a protocol that allows a classical verifier to certify (only) that a prover is not classical. We show that tests of quantumness that follow a certain template, which captures recent proposals such as (Kalai et al., 2022), can in fact do much more. Namely, the same protocols can be used for certifying a qubit, a building-block that stands at the heart of applications such as certifiable randomness and classical delegation of quantum computation. Certifying qubits was previously only known to be possible based on the hardness of the Learning with Errors problem and the use of adaptive hardcore (Brakerski et al., 2018). Our framework allows certification of qubits based only on the existence of post-quantum trapdoor claw-free functions, or on quantum fully homomorphic encryption. These can be instantiated, for example, from Ring Learning with Errors. On the technical side, we show that the quantum soundness of any such protocol can be reduced to proving a bound on a simple algorithmic task: informally, answering ``two challenges simultaneously'' in the protocol. Our reduction formalizes the intuition that these protocols demonstrate quantumness by leveraging the impossibility of rewinding a general quantum prover. This allows us to prove tight bounds on the quantum soundness of (Kahanamoku-Meyer et al., 2021) and (Kalai et al., 2022), showing that no quantum polynomial-time prover can succeed with probability larger than $\cos^2 \frac{\pi}{8}\approx 0.853$. Previously, only an upper bound on the success probability of classical provers, and a lower bound on the success probability of quantum provers, were known. We then extend this proof of quantum soundness to show that provers that approach the quantum soundness bound must perform almost anti-commuting measurements. This certifies that the prover holds a qubit., Comment: 27 pages; small typos fixed

Experimental evidence of novel phenomena in hydrogenated graphite fibers is found. An indirect excitonic mechanism is likely leading to a SC state below the temperature Tc = 50 K, where the gap is divergent. Analysis of the gap within the framework provided by the Bardeen-Cooper-Schrieffer (BCS) theory of superconductivity shows that this is a multigap system. The energy gap data can be better explained within the framework of topologically protected flat bands applied to systems in which superconductivity occurs on the surface or at the internal interfaces of the samples. The temperature dependence of the SC gap is linear above 50 K. We use nonlocal differential conductance Gdiff(V) = dI(V)/dV experimental data to show clear evidence of topological phenomena such as interference of chiral asymmetric Andreev edge states and crossed Andreev conversion. Gdiff(V) has a negative part that results from the nonlocal coherence between electron and holes in the Andreev edge states. We conclude that hydrogenated graphite bears the marks of an unconventional high-temperature superconductor (HTSC)., Comment: 5 pages, 7 figures. arXiv admin note: substantial text overlap with arXiv:2005.05876

The use of logical systems for problem-solving may be as diverse as in proving theorems in mathematics or in figuring out how to meet up with a friend. In either case, the problem solving activity is captured by the search for an \emph{argument}, broadly conceived as a certificate for a solution to the problem. Crucially, for such a certificate to be a solution, it has be \emph{valid}, and what makes it valid is that they are well-constructed according to a notion of inference for the underlying logical system. We provide a general framework uniformly describing the use of logic as a mathematics of reasoning in the above sense. We use proof-theoretic validity in the Dummett-Prawitz tradition to define validity of arguments, and use the theory of tactical proof to relate arguments, inference, and search., Comment: submitted

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; for example, one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of reduction is to obtain a tool for uniform and modular treatment of proof theory and provide a bridge between semantics logics and their proof theory. The article discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics. The results include the following: a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and, a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic.

We give a comprehensive characterization of the computational power of shallow quantum circuits combined with classical computation. Specifically, for classes of search problems, we show that the following statements hold, relative to a random oracle: (a) $\mathsf{BPP}^{\mathsf{QNC}^{\mathsf{BPP}}} \neq \mathsf{BQP}$. This refutes Jozsa's conjecture [QIP 05] in the random oracle model. As a result, this gives the first instantiatable separation between the classes by replacing the oracle with a cryptographic hash function, yielding a resolution to one of Aaronson's ten semi-grand challenges in quantum computing. (b) $\mathsf{BPP}^{\mathsf{QNC}} \nsubseteq \mathsf{QNC}^{\mathsf{BPP}}$ and $\mathsf{QNC}^{\mathsf{BPP}} \nsubseteq \mathsf{BPP}^{\mathsf{QNC}}$. This shows that there is a subtle interplay between classical computation and shallow quantum computation. In fact, for the second separation, we establish that, for some problems, the ability to perform adaptive measurements in a single shallow quantum circuit, is more useful than the ability to perform polynomially many shallow quantum circuits without adaptive measurements. (c) There exists a 2-message proof of quantum depth protocol. Such a protocol allows a classical verifier to efficiently certify that a prover must be performing a computation of some minimum quantum depth. Our proof of quantum depth can be instantiated using the recent proof of quantumness construction by Yamakawa and Zhandry [STOC 22]., Comment: 104 pages (+ 9 page Appendix), 10 figures

We give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with eigenworlds (i.e., generic representatives of worlds) in an arbitrary model. This reasoning is captured by a sequent calculus for a meta-logic (in this case, first-order classical logic) expressive enough to capture the semantics of the object-logic. Essentially, one has a calculus of validity for the object-logic. The method proceeds through the perspective of reductive logic (as opposed to the more traditional paradigm of deductive logic), using the space of reductions as a medium for showing the behavioural equivalence of reduction in the sequent calculus for the object-logic and in the validity calculus. Rather than study the technique in general, we illustrate it for the logic of Bunched Implications (BI), thus IPL and MILL (without negation) are also treated. Intuitively, BI is the free combination of intuitionistic propositional logic and multiplicative intuitionistic linear logic, which renders its meta-theory is quite complex. The literature on BI contains many similar, but ultimately different, algebraic structures and satisfaction relations that either capture only fragments of the logic (albeit large ones) or have complex clauses for certain connectives (e.g., Beth's clause for disjunction instead of Kripke's). It is this complexity that motivates us to use BI as a case-study for this approach to semantics., Comment: accepted

Proof-theoretic semantics (P-tS) is the approach to meaning in logic based on 'proof' (as opposed to 'truth'). There are two major approaches to P-tS: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a semantics of arguments, and the latter is a semantics of logical constants. This paper demonstrates that the B-eS for intuitionistic propositional logic (IPL) encapsulates the declarative content of a version of P-tV based on the elimination rules. This explicates how the B-eS for IPL works, and shows the completeness of this version of P-tV.

Proof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-eS). This semantics is given by a relation called support, explaining the meaning of the logical constants, which is parameterized by systems of rules called bases that provide the semantics of atomic propositions. In this paper, we interpret bases as collections of definite formulae and use the operational view of the latter as provided by uniform proof-search -- the proof-theoretic foundation of logic programming (LP) -- to establish the completeness of IPL for the B-eS. This perspective allows negation, a subtle issue in P-tS, to be understood in terms of the negation-as-failure protocol in LP. Specifically, while the denial of a proposition is traditionally understood as the assertion of its negation, in B-eS we may understand the denial of a proposition as the failure to find a proof of it. In this way, assertion and denial are both prime concepts in P-tS., Comment: submitted

A test of quantumness is a protocol where a classical user issues challenges to a quantum device to determine if it exhibits non-classical behavior, under certain cryptographic assumptions. Recent attempts to implement such tests on current quantum computers rely on either interactive challenges with efficient verification, or non-interactive challenges with inefficient (exponential time) verification. In this paper, we execute an efficient non-interactive test of quantumness on an ion-trap quantum computer. Our results significantly exceed the bound for a classical device's success., Comment: 6 pages, 2 figures

Unique to certain unconventional superconductors is the coexistence of magnetism and superconductivity. We have previously found ferromagnetism and superconductivity in hydrogenated graphitic materials. Herein we present similar as well as completely new findings this time applicable to hydrogenated graphite foils. As the strength of the magnetic field is increased, the temperature-dependent magnetization shows several important transitions. From a Neel paramagnetic-antiferromagnetic transition, to a ferromagnetic superconductor state, to an orbital paramagnetic glass high-temperature superconductor with critical temperature for the dominant phase at Tc = 50 to 60 K. The ferromagnetic state is observed up to room temperature. Thus, the magnetism of hydrogenated low-density carbon graphite foils plays an important role in establishing electronic correlations of which some are superconducting in nature., Comment: 23 pages, 12 figures

In our previous work, high-temperature superconductivity (HTSC) was probed for the first time by using electrical differential conductance Gdiff(V) = dI/dV data as obtained from current-voltage V(I) measurements on a hydrogenated graphitic fiber [1]. While our nonlocal method for finding the superconducting (SC) gap was recently applied to a conventional SC (Pb [2]), the nonlocal Gdiff method was first proposed in [1]. Herein, we are bringing forth an update on the topic., Comment: 9 pages, 3 figures. arXiv admin note: text overlap with arXiv:2005.05876