Zobrazeno 1 - 9
of 9
pro vyhledávání: '"Dan Hernest"'
Autor:
Dan Hernest, Trifon Trifonov
Publikováno v:
Logical Methods in Computer Science, Vol Volume 17, Issue 4 (2021)
We adapt our light Dialectica interpretation to usual and light modal formulas (with universal quantification on boolean and natural variables) and prove it sound for a non-standard modal arithmetic based on Goedel's T and classical S4. The range of
Externí odkaz:
https://doaj.org/article/0cd1c9e73c424675bf5ebcf53a3d5157
Autor:
Dan Hernest, Trifon Trifonov
Our Minlog (http://minlog-system.de) variant and implementation of modal Dialectica (https://arxiv.org/pdf/1212.0020) may be found athttps://triffon.github.io/mlfd. This is the appendix of our Modal Functional Interpretation paper, as submitted tohtt
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7405135aeb6367194cf780c84bb99e5f
Autor:
Mircea-Dan Hernest, Trifon Trifonov
Publikováno v:
Annals of Pure and Applied Logic. 161:1379-1389
We upgrade the light Dialectica interpretation (Hernest, 2005) [6] by adding two more light universal quantifiers, which are both semi-computational and semi-uniform and complement each other. An illustrative example is presented for the new light qu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::04e066ed1442138d9b63d3f346053259
https://doi.org/10.1016/j.apal.2010.04.008
https://doi.org/10.1016/j.apal.2010.04.008
Autor:
Mircea-Dan Hernest
Publikováno v:
MLQ. 55:551-561
Osterreich In view of an enhancement of our implementation on the computer, we explore the possibility of an algorithmic optimization of the various proof-theoretic techniques employed by Kohlenbach for the synthesis of new (and better) effective uni
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d08088156fdf05bc11acae74eedda55e
https://doi.org/10.1002/malq.200710093
https://doi.org/10.1002/malq.200710093
Autor:
Mircea-Dan Hernest, Ulrich Kohlenbach
Publikováno v:
Hernest, M-D & Kohlenbach, U 2005, ' A complexity analysis of functional interpretations ', Theoretical Computer Science, vol. 338, no. 1-3, pp. 200-246 .
BRICS Report Series; No 12 (2003): RS-12 A Complexity Analysis of Functional Interpretations.
BRICS Report Series; Nr. 12 (2003): RS-12 A Complexity Analysis of Functional Interpretations.
Hernest, M-D & Kohlenbach, U 2003, ' A Complexity Analysis of Functional Interpretations ' B R I C S Report Series, no. RS-03-12 .
BRICS Report Series; No 12 (2003): RS-12 A Complexity Analysis of Functional Interpretations.
BRICS Report Series; Nr. 12 (2003): RS-12 A Complexity Analysis of Functional Interpretations.
Hernest, M-D & Kohlenbach, U 2003, ' A Complexity Analysis of Functional Interpretations ' B R I C S Report Series, no. RS-03-12 .
Summary: We give a quantitative analysis of Gödel's functional interpretation and its monotone variant. The two have been used for the extraction of programs and numerical bounds as well as for conservation results. They apply both to (semi-)intuiti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0e468d834abc9ae505b64b8a5c6a459b
https://doi.org/10.1016/j.tcs.2004.12.019
https://doi.org/10.1016/j.tcs.2004.12.019
Autor:
Paulo Oliva, Mircea-Dan Hernest
Publikováno v:
Logic and Theory of Algorithms ISBN: 9783540694052
CiE
CiE
We show how different functional interpretations can be combined via a multi-modal linear logic. A concrete hybrid of Kreisel's modified realizability and Godel's Dialectica is presented, and several small applications are given. We also discuss how
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b4145cb25ac64c267b47ad6771dcfd02
https://doi.org/10.1007/978-3-540-69407-6_29
https://doi.org/10.1007/978-3-540-69407-6_29
Autor:
Mircea-Dan Hernest
Publikováno v:
Computer Science Logic ISBN: 9783540282310
CSL
CSL
We give a Natural Deduction formulation of an adaptation of Godel's functional (Dialectica) interpretation to the extraction of (more) efficient programs from (classical) proofs. We adapt Jorgensen's formulation of pure Dialectica translation by elim
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4937043bccb0910c51713fd2617ad1c9
https://doi.org/10.1007/11538363_33
https://doi.org/10.1007/11538363_33
Autor:
Mircea-Dan Hernest
Publikováno v:
Electronic Notes in Theoretical Computer Science. (3):43-53
We demonstrate program extraction by the Light Dialectica Interpretation (LDI) on a minimal logic proof of the classical existence of Fibonacci numbers. This semi-classical proof is available in MinLog's library of examples. The term of Gödel's T ex
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::037df4da3404ad0a6d053123b0ac2f72
Autor:
Mircea-Dan Hernest
Publikováno v:
Electronic Notes in Theoretical Computer Science. (5):141-149
We extract on the computer a number of moduli of uniform continuity for the first few elements of a sequence of closed terms t of Godel's T of type (N->N)->(N->N). The generic solution may then be quickly inferred by the human. The automated synthesi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a2997cf83895d2a79bac11fa3cd28062