## Found 800 Documents (Results 1–100)

100
MathJax

### Logic and verification of product configuration in the automotive industry. (English)Zbl 07543891

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 387-408 (2022).
Full Text:

### The Braga method: extracting certified algorithms from complex recursive schemes in Coq. (English)Zbl 07543890

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 305-386 (2022).
Full Text:

### An Ad-Hoc semantics to study structural properties of types. (English)Zbl 07543889

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 267-303 (2022).
Full Text:

### Formal topology and univalent foundations. (English)Zbl 07543888

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 255-266 (2022).
Full Text:

### A uniform characterization of $$\Sigma_1$$-reflection over the fragments of Peano arithmetic. (English)Zbl 07543887

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 189-253 (2022).
Full Text:

### Generalized spaces for constructive algebra. (English)Zbl 07543886

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 99-187 (2022).
Full Text:

### From intuitionistic mathematics to point-free topology. (English)Zbl 07543885

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 55-98 (2022).
Full Text:

### Conceptions of proof from aristotle to Gentzen’s calculi. (English)Zbl 07543884

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 33-54 (2022).
Full Text:

### Proof and computation: perspectives for mathematics, computer science, and philosophy. (English)Zbl 07543883

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 1-32 (2022).
Full Text:

Full Text:

### The Jacobson radical for an inconsistency predicate. (English)Zbl 07527242

MSC:  13-XX 03Dxx 03Fxx
Full Text:

### Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. (English)Zbl 07380372

Hackensack, NJ: World Scientific (ISBN 978-981-12-3647-1/hbk; 978-981-12-3649-5/ebook). xvi, 408 p. (2022).
Full Text:

Full Text:

### A semilattice of degrees of computable metrics. (English. Russian original)Zbl 07401177

Sib. Math. J. 62, No. 5, 822-841 (2021); translation from Sib. Mat. Zh. 62, No. 5, 1013-1038 (2021).
MSC:  03Dxx 03Fxx 68Qxx
Full Text:

### An example of noncomputability of exponents of a system of ordinary differential equations. (English. Russian original)Zbl 07392395

Mosc. Univ. Math. Bull. 76, No. 2, 53-59 (2021); translation from Vestn. Mosk. Univ., Ser. I 76, No. 2, 10-15 (2021).
MSC:  03Dxx 03-XX 03Fxx
Full Text:

### The complexity of module radicals. (English)Zbl 07391980

MSC:  03D80 03F65
Full Text:

### Dense computability structures. (English)Zbl 07371884

MSC:  03Fxx 68Qxx 03Dxx
Full Text:

MSC:  03Dxx
Full Text:

Full Text:

Full Text:

Full Text:

### The constructive Hahn-Banach theorem, revisited. (English)Zbl 07377989

Rezuş, Adrian (ed.), Contemporary logic and computing. London: College Publications. Landsc. Log. 1, 638-663 (2020).
MSC:  03Bxx 03Dxx

Full Text:

Full Text:

### Well-partial orderings and their maximal order types. (English)Zbl 07218748

Schuster, Peter M. (ed.) et al., Well-quasi orders in computation, logic, language and reasoning. A unifying concept of proof theory, automata theory, formal languages and descriptive set theory. Based on the minisymposium on well-quasi orders: from theory to applications within the Jahrestagung der Deutschen Mathematiker-Vereinigung (DMV), Hamburg, Germany, September 21–25, 2015 and the Dagstuhl seminar 16031 on well quasi-orders in computer science, Schloss Dagstuhl, Germany, January 17–22, 2016. Cham: Springer. Trends Log. Stud. Log. Libr. 53, 351-391 (2020).
MSC:  03Fxx 03Exx 03Dxx
Full Text:

Full Text:

Full Text:

### Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. (English)Zbl 1431.03011

Synthese Library 412. Cham: Springer (ISBN 978-3-030-20446-4/hbk; 978-3-030-20447-1/ebook). x, 374 p. (2019).
Full Text:

Full Text:

Full Text:

Full Text:

Full Text:

### Proof and computation. Digitization in mathematics, computer science, and philosophy. Based on the international autumn school “Proof and computation”, Fischbachau, Germany, October 3–8, 2016. (English)Zbl 1400.03005

Hackensack, NJ: World Scientific (ISBN 978-981-3270-93-0/hbk; 978-981-3270-95-4/ebook). viii, 291 p. (2018).
Full Text:

### On fixed-point theorems in synthetic computability. (English)Zbl 1403.03076

MSC:  03D75 54H25 03F65
Full Text:

Full Text:

Full Text:

### The computational content of nonstandard analysis. (English)Zbl 07440186

Kohlenbach, Ulrich (ed.) et al., Proceedings of the sixth international workshop on classical logic and computation, CL&C 2016, Porto, Portugal, June 23, 2016. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 213, 24-40 (2016).
Full Text:

### A constructive manifestation of the Kleene-Kreisel continuous functionals. (English)Zbl 1402.03020

MSC:  03B15 03F50 03C90 03D65
Full Text:

### Limit spaces with approximations. (English)Zbl 1432.03083

MSC:  03D75 03D80 03F60
Full Text:

### Finite choice, convex choice and finding roots. (English)Zbl 1448.03052

MSC:  03F60 03D30 03D78
Full Text:

### Intuitionistic provability versus uniform provability in $$\mathsf{RCA}$$. (English)Zbl 1461.03009

Beckmann, Arnold (ed.) et al., Evolving computability. 11th conference on computability in Europe, CiE 2015, Bucharest, Romania, June 29 – July 3, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9136, 186-195 (2015).
Full Text:

### Computation, proof, machine. Mathematics enters a new age. Translated from the French by Pierre Guillot and Marion Roman. (English)Zbl 1318.01002

Cambridge: Cambridge University Press (ISBN 978-0-521-13377-7/pbk; 978-0-521-11801-9/hbk). viii, 152 p. (2015).

### The extensional realizability model of continuous functionals and three weakly non-constructive classical theorems. (English)Zbl 1448.03053

MSC:  03F60 03D65
Full Text:

Full Text:

Full Text:

### Reverse mathematics, countable and uncountable. (English)Zbl 1329.03046

Greenberg, Noam (ed.) et al., Effective mathematics of the uncountable. Cambridge: Cambridge University Press; Ithaca, NY: Association for Symbolic Logic (ASL) (ISBN 978-1-107-01451-0/hbk; 978-1-139-02859-2/ebook). Lecture Notes in Logic 41, 150-163 (2013).

Full Text:

Full Text:

Full Text:

Full Text:

### The metamorphoses of the calculus. An amazing history of mathematics. Reprint of the 2007 edition. (Les métamorphoses du calcul. Une étonnante histoire de mathématiques.) (French)Zbl 1360.01012

Poche. Paris: Éditions Le Pommier (ISBN 978-2-7465-0561-2/pbk). 224 p. (2011).

Full Text:

Full Text:

### Towards a formal theory of computability. (English)Zbl 1245.03064

Schindler, Ralf (ed.), Ways of proof theory. Collected papers by speakers of the colloquium and workshop held on the occasion of the retirement of Wolfram Pohlers, July 17–19, 2008, Münster, Germany. Frankfurt am Main: Ontos Verlag (ISBN 978-3-86838-087-3/hbk). Ontos Mathematical Logic 2, 257-282 (2010).
MSC:  03D65 03F65

Full Text:

### On computably locally compact Hausdorff spaces. (English)Zbl 1159.03044

MSC:  03F60 03F65 03D80
Full Text:

### Mathematical logic with special reference to the natural numbers. Paperback reprint of the 1972 edition. (English)Zbl 1156.03002

Cambridge: Cambridge University Press (ISBN 978-0-521-09058-2/pbk). xvi, 638 p. (2008).

### Classical truth in higher types. (English)Zbl 1140.03037

MSC:  03F10 03B15 03D65 03E25 03F50
Full Text:

### Recursion on the partial continuous functionals. (English)Zbl 1137.03035

Dimitracopoulos, Costas (ed.) et al., Logic colloquium 2005. Proceedings of the annual European summer meeting of the Association for Symbolic Logic (ASL), Athens, Greece, July 28–August 3, 2005. Cambridge: Cambridge University Press; Urbana, IL: Association for Symbolic Logic (ASL) (ISBN 978-0-521-88425-9/hbk). Lecture Notes in Logic 28, 173-201 (2008).
MSC:  03F65 03D65 03D75

### The metamorphoses of the calculus. An amazing history of mathematics. (Les métamorphoses du calcul. Une étonnante histoire de mathématiques.) (French)Zbl 1161.01001

Paris: Éditions Le Pommier (ISBN 978-2-7465-0324-3/pbk). 224 p. (2007).

### First steps in synthetic computability theory. (English)Zbl 1273.03144

Escardó, M. (ed.) et al., Proceedings of the 21st annual conference on mathematical foundations of programming semantics (MFPS XXI), University of Birmingham, Birmingham, UK, May 18–21, 2005. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 155, 5-31 (2006).
Full Text:

### On local non-compactness in recursive mathematics. (English)Zbl 1095.03034

MSC:  03D80 03F60 54E35
Full Text:

### Proving as a computable procedure. (English)Zbl 1091.03029

MSC:  03F99 03D99

### $$\Pi_1^0$$ classes – structure and applications. (English)Zbl 0962.03040

Cholak, Peter A. (ed.) et al., Computability theory and its applications. Current trends and open problems. Proceedings of a 1999 AMS-IMS-SIAM joint summer research conference, Boulder, CO, USA, June 13-17, 1999. Providence, RI: American Mathematical Society (AMS). Contemp. Math. 257, 39-59 (2000).

### Computability. Computable functions, logic, and the foundations of mathematics. With “Computability and undecidability—a timeline. The story of the development of computable functions and the undecidability of arithmetic to 1970” by Richard L. Epstein. 2nd ed. (English)Zbl 0951.03001

Belmont, CA: Wadsworth/Thomson Learning. 299 p., 38 p. (2000).

### Explicit mathematics with the monotone fixed point principle II: Models. (English)Zbl 0930.03093

MSC:  03F50 03F35 03F65
Full Text:

### The contribution of Polish logicians to recursion theory. (English)Zbl 1018.03005

Kijania-Placek, Katarzyna (ed.) et al., The Lvov-Warsaw school and contemporary philosophy. Papers from the conference, Lviv (Lvov), Ukraine, November 15-17, 1995 and Warsaw, Poland, November 19-21, 1995. Dordrecht: Kluwer Academic Publishers. Synth. Libr. 273, 265-282 (1998).
MSC:  03-03 03Dxx 01A60

Full Text:

### Kreiseliana: about and around Georg Kreisel. (English)Zbl 0894.03002

Wellesley, MA: A K Peters. xiii, 495 p. (1996).

### Kreisel, generalized recursion theory and me. (English)Zbl 0895.01007

Odifreddi, Piergiorgio (ed.), Kreiseliana: about and around Georg Kreisel. Wellesley, MA: A K Peters. 103-106 (1996).
MSC:  01A70 03-03 03D60

### Density and choice for total continuous functionals. (English)Zbl 0901.03039

Odifreddi, Piergiorgio (ed.), Kreiseliana: about and around Georg Kreisel. Wellesley, MA: A K Peters. 335-362 (1996).

Full Text:

Full Text:

### Computational foundations of basic recursive function theory. (English)Zbl 0798.03046

MSC:  03D75 03F65 03B35
Full Text:

### Recursion theory for metamathematics. (English)Zbl 0796.03003

Oxford Logic Guides. 22. New York: Oxford University Press. xiv, 163 p. (1993).

### A simple and powerful approach for studying constructivity, computability, and complexity. (English)Zbl 1434.03114

Myers, J. Paul jun. (ed.) et al., Constructivity in computer science. Summer symposium, San Antonio, TX, June 19–22, 1991. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 613, 228-246 (1992).
MSC:  03D75 03F65
Full Text:

Full Text:

### Some properties of the syntactic p-recursion categories generated by consistent, recursively enumerable extensions of Peano arithmetic. (English)Zbl 0745.03037

Reviewer: P.Bankston
MSC:  03D75 18B99 03F99
Full Text:

### Monotone inductive definitions in a constructive theory of functions and classes. (English)Zbl 0665.03037

Reviewer: V.Yu.Sazonov
MSC:  03D70 03F65 03D75
Full Text:

### Languages, effectivity and constructive mathematics. (English)Zbl 0667.03036

Languages, logic, mathematical linguistics, Pap. 2nd Natl. Colloq., Braşov/Rom. 1988, 47-57 (1988).
Reviewer: C.Calude
MSC:  03D80 03F65

### Kleene computable functionals and the higher order existence property. (English)Zbl 0647.03048

Reviewer: P.Bankston
Full Text:

Full Text:

### Reducibilities of sets based on constructive functions of a real variable. (English)Zbl 0646.03038

Reviewer: B.van Rootselaar
MSC:  03D30 03F65
Full Text:

### Induktive Definitionen und Dilatoren. (Inductive definitions and dilators). (German)Zbl 0642.03034

Reviewer: W.Buchholz
MSC:  03F99 03D70 03D60
Full Text:

### Representations of the real numbers and of the open subsets of the set of real numbers. (English)Zbl 0643.03041

Reviewer: K.Weihrauch
Full Text:

### The use of ordinals in the constructive foundations of mathematics. (English)Zbl 0623.03052

Logic, methodology and philosophy of science VII, Proc. 7th Int. Congr., Salzburg 1983, Stud. Logic Found. Math. 114, 83-94 (1986).
Reviewer: H.Pfeiffer

### Transcendental numbers and eventual dominance of exponential functions. (English)Zbl 0621.03029

Reviewer: P.Clote
MSC:  03D30 03F99
Full Text:

### Ein Kriterium für die konstruktive Lösbarkeit der Differentialgleichung $$y'=f(x,y)$$. (German)Zbl 0553.03037

MSC:  03F65 34A99 03D60
Full Text:

### Mathematical logic. Complementary chapters. Textbook. (Matematicheskaya logika. Dopolnitel’nye glavy. Uchebnoe posobie). (Russian)Zbl 0591.03002

Moskva: Izdatel’stvo Moskovskogo Universiteta. 120 p. R. 0.25 (1984).
Reviewer: I.H.Bekker

### Arithmetic complexity of differentiation in constructive mathematics. (Russian)Zbl 0582.03049

MSC:  03F65 03D30 26A24
Full Text:

all top 5

all top 5

all top 5

all top 3

all top 3