Showing 2019Show all
3 papers · 1 filter
cs.LO2019
Extraction of Efficient Programs in -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, 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…
math.LO2019
Efficient elimination of Skolem functions in
Ján Komara
Elimination of a single Skolem function in pure logic increases the length of proofs only linearly. The result is shown for derivations with cuts that are free for the Skolem funct…