arXiv subjects

Paul J. Voda

Publications and source records attributed to Paul J. Voda.

3 recordsLinked to original sources

arXiv2019

Extraction of Efficient Programs in $IΣ_1$-arithmetic

Clausal Language (CL) is a declarative programming and verifying system used in our teaching of computer science. CL is an implementation of, what we call, $\mathit{PR}{+}IΣ_1$ paradigm (primitive recursive functions with $IΣ_1$-arithmetic). This paper introduces an extension of $IΣ_1$-proofs called extraction proofs where one can extract from the proofs of $Π_2$-specifications primitive recursive programs as efficient as the hand-coded ones. This is achieved by having the programming constructs correspond exactly to the proof rules with the computational content.

cs.LO↗

arXiv2019

On Herbrand Skeletons

Herbrand's theorem plays an important role both in proof theory and in computer science. Given a Herbrand skeleton, which is basically a number specifying the count of disjunctions of the matrix, we would like to get a computable bound on the size of terms which make the disjunction into a quasitautology. This is an important problem in logic, specifically in the complexity of proofs. In computer science, specifically in automated theorem proving, one hopes for an algorithm which avoids the guesses of existential substitution axioms involved in proving a theorem. Herbrand's theorem forms the very basis of automated theorem proving where for a given number $n$ we would like to have an algorithm which finds the terms in the $n$ disjunctions of matrices solely from the shape of the matrix. The main result of this paper is that both problems have negative solutions.

math.LO↗

arXiv2017

First- and Second-Order Models of Recursive Arithmetics

We study a quadruple of interrelated subexponential subsystems of arithmetic WKL$_0^-$, RCA$^-_0$, I$Δ_0$, and $Δ$RA$_1$, which complement the similarly related quadruple WKL$_0$, RCA$_0$, I$Σ_1$, and PRA studied by Simpson, and the quadruple WKL$_0^\ast$, RCA$_0^\ast$, I$Δ_0$(exp), and EFA studied by Simpson and Smith. We then explore the space of subexponential arithmetic theories between I$Δ_0$ and I$Δ_0$(exp). We introduce and study first- and second-order theories of recursive arithmetic $A$RA$_1$ and $A$RA$_2$ capable of characterizing various computational complexity classes and based on function algebras $A$, studied by Clote and others.

cs.LO↗