Showing 1–4 of 4 results for author: Komara, J

On completeness of Hausdorff hyperspaces

Authors: Ján Komara

Abstract: The Hausdorff hyperspace of a metric space consists of all its non-empty bounded closed sets and it is equipped with the Pompeiu--Hausdorff set distance. We present a simpler novel proof that the Hausdorff hyperspace of a complete space is complete as well. The Main Lemma is crucial in this demonstration and though it uses an induction argument -- the only one in our completeness proof -- it is st… ▽ More The Hausdorff hyperspace of a metric space consists of all its non-empty bounded closed sets and it is equipped with the Pompeiu--Hausdorff set distance. We present a simpler novel proof that the Hausdorff hyperspace of a complete space is complete as well. The Main Lemma is crucial in this demonstration and though it uses an induction argument -- the only one in our completeness proof -- it is stated purely in terms of neighborhoods. △ Less

Submitted 10 May, 2025; originally announced May 2025.

Comments: 5 pages

MSC Class: 54B20 (Primary) 54E35; 28A80 (Secondary)

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

Authors: Ján Komara, Paul J. Voda

Abstract: 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… ▽ More 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. △ Less

Submitted 1 October, 2019; originally announced October 2019.

Comments: 16 pages; reprint of the technical report from July, 2000

MSC Class: 03F30; 03D20 ACM Class: F.3.1; F.4.1

On Herbrand Skeletons

Authors: Paul J. Voda, Ján Komara

Abstract: 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… ▽ More 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. △ Less

Submitted 30 September, 2019; originally announced September 2019.

Comments: 24 pages; reprint of the revision of the technical report

Report number: Technical Report mff-ii-02-1995 MSC Class: 03B10 ACM Class: F.4.1

Efficient elimination of Skolem functions in $\text{LK}^{\text{h}}$

Authors: Ján Komara

Abstract: 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 function in a sequent calculus with strong locality property. 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 function in a sequent calculus with strong locality property. △ Less

Submitted 15 June, 2020; v1 submitted 4 September, 2019; originally announced September 2019.

Comments: 31 pages; generalization of main results for calculus with cuts, added section on cut elimination, added discussion on eigenvariable condition

MSC Class: 03F03; 03F20 ACM Class: F.4.1

Journal ref: Archive for Mathematical Logic 61, pages 503-534 (2022)