Výsledky vyhledávání - "Pierre Boutry"

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Autor: Filip Maric, Pierre Boutry, Danijela Simić

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2020, 65 (1), pp.31-73. ⟨10.1007/s10817-020-09551-2⟩
Journal of Automated Reasoning, 2020, 65 (1), pp.31-73. ⟨10.1007/s10817-020-09551-2⟩

We describe formalization of the Poincare disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line $$\mathbb {C}{}P^1$$ and is shown to satisfy Tarski’s axioms except for Euc

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2dbeef9930f75e15a2e1b0813d069843
https://hal.inria.fr/hal-03120829/document

Zobrazit plný text záznamu

Formalization of the Arithmetization of Euclidean Plane Geometry and Applications

Autor: Pierre Boutry, Julien Narboux, Gabriel Braun

Publikováno v: Journal of Symbolic Computation
Journal of Symbolic Computation, Elsevier, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩
James H. Davenport and Temur Kutsia
Journal of Symbolic Computation, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩

International audience; This paper describes the formalization of the arithmetization of Euclidean plane geometry in the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for its well-known metamath-ematical proper

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d19606004baeac5b5c1824c21361cd57
https://hal.inria.fr/hal-01483457/file/extended-arithmetization.pdf

Zobrazit plný text záznamu

Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq

Autor: Charly Gries, Pascal Schreck, Pierre Boutry, Julien Narboux

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩
Journal of Automated Reasoning, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩

online first; International audience; In this paper we focus on the formalization of the proofs of equivalence between different versions of Euclid's 5 th postulate. Our study is performed in the context of Tarski's neutral geometry, or equivalently

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5295cfedebbea0e5f43a1d51340f29ca
https://hal.inria.fr/hal-01178236v2/document

Zobrazit plný text záznamu

From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry

Autor: Gabriel Braun, Pierre Boutry, Julien Narboux

Publikováno v: SCSS
SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science
SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science, Mar 2016, Tokyo, Japan. pp.14-28

International audience; This paper describes the formalization of the arithmetization of Euclidean geometry in the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for its well-known metamathematical properties. T

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4bd0de30ce3cc81593075bd7ba50733f
https://hal.science/hal-01282550

Zobrazit plný text záznamu

Herbrand's theorem and non-Euclidean geometry

Autor: Pierre Boutry, Michael Beeson, Julien Narboux

Publikováno v: Bulletin of Symbolic Logic
Bulletin of Symbolic Logic, 2015, 21 (2), pp.12. ⟨10.1017/bsl.2015.6⟩
Bulletin of Symbolic Logic, Association for Symbolic Logic, 2015, 21 (2), pp.12. ⟨10.1017/bsl.2015.6⟩

We use Herbrand's theorem to give a new proof that Euclid's parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b21737acf81f388f97ade66b34288d81
http://arxiv.org/abs/1410.2239

Zobrazit plný text záznamu

Ethylene oxidation to acetic acid with Pd-V2O5 type catalysts I. Gas-solid reactions

Autor: Roger Montarnal, JoséLuis Seoane, Pierre Boutry

Publikováno v: Journal of Catalysis. 63:182-190

Palladium added to V2O5 enhances the reducibility of this oxide. The reduction can then be performed at low temperature so as to produce selectively a reduced phase with the formula V4O9. The influence of ethylene partial pressure on the initial redu

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::9d9b0ee6d8fafd484abf6e4d15cfeccb
https://doi.org/10.1016/0021-9517(80)90071-8

Zobrazit plný text záznamu

Influence of the degree of crystallinity and of the composition on the activity of MoO3-Bi2O3 catalysts

Autor: Roger Montarnal, J. Wrzyszcz, Pierre Boutry

Publikováno v: Journal of Catalysis. 13:75-82

The influence of the degree of organization of the catalyst has been examined for the oxidation of butene into butadiene on bismuth molybdate. The results obtained show that the specific activity increases when the degree of crystallization decreases

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::cab557b09903213c1a1bcf6fbffaa679
https://doi.org/10.1016/0021-9517(69)90372-8

Zobrazit plný text záznamu

The mechanism of vinyl acetate formation by gas-phase catalytic ethylene acetoxidation*1

Autor: B. Samanos, Roger Montarnal, Pierre Boutry

Publikováno v: Journal of Catalysis. 23:19-30

The synthesis of vinyl acetate by vapor phase oxidation of ethylene-acetic acid mixtures has been studied using catalysts prepared by palladium deposition on silica or alumina supports. The kinetic study of this reaction served to determine the influ

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::65c5f1dcf86bcbb1af4013bee2cf59eb
https://doi.org/10.1016/0021-9517(71)90019-4

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání