相关论文: A preliminary univalent formalization of the p-adi…
A formal description of a quantum abacus based encoding system is presented. This way of representing data for processing purposes is based on a quantum algorithm for counting qubits introduced by Lesovik et al. \cite{LesovikEtal2010} and…
A permutation-invariant quantum code on $N$ qudits is any subspace stabilized by the matrix representation of the symmetric group $S_N$ as permutation matrices that permute the underlying $N$ subsystems. When each subsystem is a complex…
The polyadic integer numbers, which form a polyadic ring, are representatives of a fixed congruence class. The basics of polyadic arithmetic are presented: prime polyadic numbers, the polyadic Euler function, polyadic division with a…
We develop a notion of cell decomposition suitable for studying weak p- adic structures (reducts of p-adic fields where addition and multiplication are not (everywhere) definable). As an example, we apply this to a language with restricted…
We describe our experience implementing a broad category-theory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we have needed substantial engineering effort to teach Coq to…
In this we give a detailed proof of fermionic p-adic q-measures on Z_p and we will treat some interesting formulae related q-extension of Euler numbers and polynomials.
We survey the progress (or lack thereof!) that has been made on some questions about the p-adic slopes of modular forms that were raised by the first author in [Buz05], discuss strategies for making further progress, and examine other…
In this paper, we give p-adic q-integral representation for the Kim's q-Bernstein polynomials and we give some interesting formulae realted to Carlitz's q-Bernoulli numbers.
Gentzen's 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of mathematics. We provide here a modified version of the proof, based on G\"{o}del's reformulation, and including additional details…
The aim of this paper is to review how some approximation results in commutative algebra are being used to construct equisingular deformations of singularities. The first example of such an approximation result appeared for the first time…
Different theorem provers tend to produce proof objects in different formats and this is especially the case for modal logics, where several deductive formalisms (and provers based on them) have been presented. This work falls within the…
Sets and relations are very useful concepts for defining denotational semantics. In the Coq proof assistant, curried functions to Prop are used to represent sets and relations, e.g. A -> Prop, A -> B -> Prop, A -> B -> C -> Prop, etc.…
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a…
Imprecise and incomplete specification of system \textit{configurations} threatens safety, security, functionality, and other critical system properties and uselessly enlarges the configuration spaces to be searched by configuration…
We introduce a novel quantum programming language featuring higher-order programs and quantum controlflow which ensures that all qubit transformations are unitary. Our language boasts a type system guaranteeingboth unitarity and…
Program verifiers for imperative languages such as C may be annotation-based, in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively…
Cody & Waite argument reduction technique works perfectly for reasonably large arguments but as the input grows there are no bit left to approximate the constant with enough accuracy. Under mild assumptions, we show that the result computed…
Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, "Logic and…
The purpose of this article is to define and study new invariants of topological spaces: the $p$-adic Betti numbers and the $p$-adic torsion. These invariants take values in the $p$-adic numbers and are constructed from a virtual pro-$p$…
In this project, a rather complete proof-theoretical formalization of Lambek Calculus (non-associative with arbitrary extensions) has been ported from Coq proof assistent to HOL4 theorem prover, with some improvements and new theorems.…