Filtrer vos résultats
- 43
- 8
- 18
- 15
- 11
- 6
- 1
- 6
- 3
- 51
- 5
- 1
- 1
- 1
- 3
- 3
- 1
- 3
- 2
- 2
- 2
- 3
- 2
- 1
- 6
- 1
- 1
- 3
- 2
- 1
- 1
- 1
- 2
- 3
- 2
- 2
- 1
- 1
- 1
- 50
- 1
- 49
- 9
- 7
- 5
- 4
- 4
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 51
- 6
- 4
- 4
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
51 résultats
|
|
|
triés par
|
|
|
Interactive Theorem Proving with Temporal LogicRR-2804, INRIA. 1996
Rapport
inria-00073886v1
|
||
|
|
A Generic Library for Floating-Point Numbers and Its Application to Exact ComputingTheorem Proving in Higher Order Logics, 2001, Edinburgh, United Kingdom. pp.169-184
Communication dans un congrès
hal-00157285v1
|
||
|
|
Certified, Efficient and Sharp Univariate Taylor Models in COQSYNASC 2013 - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2013, Timisoara, Romania
Communication dans un congrès
hal-00845791v2
|
||
|
|
A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective GeometryAutomated Deduction in Geometry, ADG 2010, Jul 2010, Munich, Germany. pp.51--62, ⟨10.1007/978-3-642-25070-5_3⟩
Communication dans un congrès
hal-00657901v1
|
||
|
|
Formalising Huffman's algorithm[Research Report] Università degli Studi dell'Aquila. 2004
Rapport
hal-02149909v1
|
||
|
|
Real theorem provers deserve real user-interfaces[Research Report] RR-1684, INRIA. 1992
Rapport
inria-00076907v1
|
||
|
|
Stålmarck's Algorithm in Coq: A Three-Level ApproachRR-4353, INRIA. 2002
Rapport
inria-00072235v1
|
||
|
|
Formalising Sylow's theorems in Coq[Technical Report] RT-0327, INRIA. 2006, pp.23
Rapport
inria-00113750v2
|
||
|
|
A Formalisation of the Generalised Towers of Hanoi2017
Pré-publication, Document de travail
hal-01446070v2
|
||
|
|
Foreword to the Special Focus on Formal Proofs for Mathematics and Computer ScienceInternational Journal of Mathematics and Computer Science, 2014, pp.1-3. ⟨10.1007/s11786-014-0214-9⟩
Article dans une revue
hal-01095761v1
|
||
|
|
A Formalisation of Algorithms for Sorting Network2022
Pré-publication, Document de travail
hal-03585618v2
|
||
|
|
Sudoku in Coq[Research Report] INRIA Sophia Antipolis - Méditerranée. 2006
Rapport
hal-03277886v1
|
||
Résoudre le Mini-Rubik’s CubeInterstices, 2009
Article dans une revue
hal-01350202v1
|
|||
Proof Pearl : Playing with the Tower of Hanoi FormallyITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, Italy. ⟨10.4230/LIPIcs.ITP.2021.31⟩
Communication dans un congrès
hal-03324274v1
|
|||
|
|
Proving and Computing: a Certified Version of the Buchberger's AlgorithmRR-3275, INRIA. 1997
Rapport
inria-00073414v1
|
||
|
|
Simplifying Polynomial Expressions in a Proof Assistant[Research Report] RR-5614, INRIA. 2005, pp.16
Rapport
inria-00070394v1
|
||
|
|
Formally-Proven Kosaraju's algorithm2015
Pré-publication, Document de travail
hal-01095533v2
|
||
|
|
Rigorous Polynomial Approximation using Taylor Models in CoqFourth NASA Formal Methods Symposium, NASA, Apr 2012, Norfolk, Virginia, United States. pp.15
Communication dans un congrès
ensl-00653460v2
|
||
|
|
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and IsabelleITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 - 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩
Communication dans un congrès
hal-02303987v1
|
||
|
|
Formalizing Stalmarck's algorithm in CoqTheorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, 2000, Portland, United States. pp.388
Communication dans un congrès
hal-00150915v1
|
||
|
|
Formally verified certificate checkers for hardest-to-round computationJournal of Automated Reasoning, 2015, 54 (1), pp.1-29. ⟨10.1007/s10817-014-9312-2⟩
Article dans une revue
hal-00919498v2
|
||
|
|
A Machine-Checked Proof of the Odd Order TheoremITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩
Communication dans un congrès
hal-00816699v1
|
||
|
|
A Flexible Proof Format for SMT: a ProposalFirst International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
Communication dans un congrès
hal-00642544v1
|
||
|
|
Porting the Mathematical Components library to Hierarchy Builderthe COQ Workshop 2021, Jul 2021, virtuel- Rome, Italy
Communication dans un congrès
hal-03463762v1
|
||
|
|
Extracting Text from ProofsRR-2459, INRIA. 1995
Rapport
inria-00074217v1
|
||
|
|
Proof Certificates for Algebra and their Application to Automatic Geometry Theorem ProvingThomas Sturm; Christoph Zengler. Automated Deduction in Geometry, 6301, Springer, pp.42-59, 2011, Lecture Notes in Computer Science, 978-3-642-21045-7. ⟨10.1007/978-3-642-21046-4_3⟩
Chapitre d'ouvrage
hal-01112767v1
|
||
|
|
Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving7th International Workshop, ADG 2008, Sep 2008, Shangai, China. pp.42-59, ⟨10.1007/978-3-642-21046-4_3⟩
Communication dans un congrès
inria-00504719v1
|
||
|
|
Distant decimals of $π$Journal of Automated Reasoning, 2018, 61, pp.33-71. ⟨10.1007/s10817-017-9444-2⟩
Article dans une revue
hal-01582524v2
|
||
|
|
Playing with the Tower of Hanoi Formally2020
Pré-publication, Document de travail
hal-02903548v2
|
||
|
|
A Modular Integration of SAT/SMT Solvers to Coq through Proof WitnessesCPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨10.1007/978-3-642-25379-9_12⟩
Communication dans un congrès
istex
hal-00639130v1
|
- 1
- 2