Results 1 to 10 of about 344,169 (311)
Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma [PDF]
Electronic Proceedings in Theoretical Computer Science, 2012 We use Gödel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable well-quasi-orders) in which ...
Thomas Powell
doaj +4 more sources
The Completeness of Propositional Resolution: A Simple and Constructive Proof [PDF]
Logical Methods in Computer Science, 2006 It is well known that the resolution method (for propositional logic) is complete. However, completeness proofs found in the literature use an argument by contradiction showing that if a set of clauses is unsatisfiable, then it must have a resolution ...
Jean Gallier
doaj +5 more sources
Limits of real numbers in the binary signed digit representation [PDF]
Logical Methods in Computer Science, 2022 We extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digits.
Franziskus Wiesnet, Nils Köpp
doaj +1 more source
Algorithm and proof as Ω-invariance and transfer: A new model of computation in nonstandard analysis [PDF]
Electronic Proceedings in Theoretical Computer Science, 2014 We propose a new model of computation based on nonstandard analysis. Intuitively, the role of "algorithm" is played by a new notion of finite procedure, called Omega-invariance and inspired by physics, from nonstandard analysis.
Sam Sanders
doaj +1 more source
Central and Local Limit Theorems for Numbers of the Tribonacci Triangle
Mathematics, 2021 In this research, we continue studying limit theorems for combinatorial numbers satisfying a class of triangular arrays. Using the general results of Hwang and Bender, we obtain a constructive proof of the central limit theorem, specifying the rate of ...
Igoris Belovas
doaj +1 more source
On Nested Sequents for Constructive Modal Logics [PDF]
Logical Methods in Computer Science, 2015 We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5.
Lutz Strassburger +2 more
doaj +1 more source
The RedPRL Proof Assistant (Invited Paper) [PDF]
Electronic Proceedings in Theoretical Computer Science, 2018 RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory.
Carlo Angiuli +4 more
doaj +1 more source
On the linearized system of elasticity in the half-space
AIMS Mathematics, 2022 The purpose of this paper is twofold. The first goal is to provide a simple and constructive proof of Korn inequalities in half-space with weighted norms. The proof leads to explicit values of the constants.
Nabil Kerdid
doaj +1 more source
Human and constructive proof of combinatorial identities: an example from Romik [PDF]
Discrete Mathematics & Theoretical Computer Science, 2005 It has become customary to prove binomial identities by means of the method for automated proofs as developed by Petkovšek, Wilf and Zeilberger. In this paper, we wish to emphasize the role of "human'' and constructive proofs in contrast with the ...
D. Merlini, R. Sprugnoli, M. C. Verri
doaj +1 more source
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics [PDF]
Logical Methods in Computer Science, 2008 Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible.
Robert Constable, Wojciech Moczydlowski
doaj +1 more source