Paul J. Voda

collaborators

3 papers

cs.LO2019

Extraction of Efficient Programs in $I Σ_{1}$ -arithmetic

Ján Komara, Paul J. Voda

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, $PR + I Σ_{1}$ par…

math.LO2019

On Herbrand Skeletons

Paul J. Voda, Ján Komara

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…

cs.LO2017

First- and Second-Order Models of Recursive Arithmetics

Ján Kľuka, Paul J. Voda

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}$ ,…

Extraction of Efficient Programs in IΣ1​-arithmetic

On Herbrand Skeletons

First- and Second-Order Models of Recursive Arithmetics

Extraction of Efficient Programs in $I Σ_{1}$ -arithmetic