Zobrazeno 1 - 10
of 18
pro vyhledávání: '"Guenot, Nicolas"'
Autor:
Guenot, Nicolas
Cette thèse s'intéresse à l'usage des formalismes d'inférence profonde comme fondement des interprétations calculatoires des systèmes de preuve, en suivant les deux approches principales: celle des preuves comme programmes et celle de la recher
Externí odkaz:
http://pastel.archives-ouvertes.fr/pastel-00929908
http://pastel.archives-ouvertes.fr/docs/00/92/99/08/PDF/thesis.pdf
http://pastel.archives-ouvertes.fr/docs/00/92/99/08/PDF/thesis.pdf
Autor:
Guenot, Nicolas, Gustafsson, Daniel
Publikováno v:
EPTCS 185, 2015, pp. 102-109
Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in equational style
Externí odkaz:
http://arxiv.org/abs/1507.08056
Autor:
Brock-Nannestad, Taus, Guenot, Nicolas
Publikováno v:
EPTCS 176, 2015, pp. 24-33
We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a standard focused system, related to the constraints in grouping rule inst
Externí odkaz:
http://arxiv.org/abs/1502.04771
Autor:
Brock-Nannestad, Taus, Guenot, Nicolas
Publikováno v:
In Electronic Notes in Theoretical Computer Science 21 December 2015 319:103-119
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Publikováno v:
Politische Ökologie; jul2021, Issue 164/165, p81-86, 6p
Autor:
Guenot, Nicolas
Publikováno v:
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English
This thesis investigates the use of deep inference formalisms as basis for a computational interpretation of proof systems, following the two main approaches: proofs-as-programs and proof-search-as-computation. The first contribution is the developme
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______212::b838a33177aee85f2a3f31783cc61c7c
https://pastel.archives-ouvertes.fr/pastel-00929908/document
https://pastel.archives-ouvertes.fr/pastel-00929908/document
Publikováno v:
20th EACSL Annual Conference on Computer Science Logic
20th EACSL Annual Conference on Computer Science Logic, Sep 2011, Bergen, Norway. pp.159-173, ⟨10.4230/LIPIcs.CSL.2011.159⟩
20th EACSL Annual Conference on Computer Science Logic, Sep 2011, Bergen, Norway. pp.159-173, ⟨10.4230/LIPIcs.CSL.2011.159⟩
International audience; The focusing theorem identifies a complete class of sequent proofs that have no inessential non-deterministic choices and restrict the essential choices to a particular normal form. Focused proofs are therefore well suited bot
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::773f77c06814df0f04ad70a37b44292e
https://inria.hal.science/hal-00772420/file/paper88.pdf
https://inria.hal.science/hal-00772420/file/paper88.pdf
Autor:
Guenot, Nicolas
The proof-theoretic approach to logic programming has benefited from the introduction of focused proof systems, through the non-determinism reduction and control they provide when searching for proofs in the sequent calculus. However, this technique
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4fc0e3450888db59baa7d489994bc041
Publikováno v:
ACM International Conference Proceeding Series; 7/17/2014, p1-8, 8p