-
Notifications
You must be signed in to change notification settings - Fork 3
/
index.html
109 lines (93 loc) · 9.06 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>Dedukti - a Logical Framework</title>
<link rel="stylesheet" href="style/style.css">
<link rel="icon" href="img/favicon.png">
</head>
<body>
<div id="header">
<img src="img/dedukti.png" alt="Dedukti Logo" class="logo"/>
</div>
<div id="main">
<h1 class="title">A Logical Framework</h1>
<h2>What is Dedukti?</h2>
<p>Dedukti is a logical framework based on the λΠ-calculus modulo in which many theories and logics can be expressed.</p>
<h2>Where does the name "Dedukti" comes from?</h2>
<p>"Dedukti" means "to deduce" in <a href="http://en.wikipedia.org/wiki/Esperanto">Esperanto</a>.</p>
<h2>How to get/install/use Dedukti?</h2>
<p>See the <a href="https://github.com/Deducteam/Dedukti">GitHub repository</a>.</p>
<p>See the <a href="https://github.com/Deducteam/Dedukti/blob/master/README.md">manual</a> for the current version (v2.5.1) of Dedukti.</p>
<p>There is also a <a href="tutorial.html">tutorial</a>.</p>
<h2>Dedukti libraries</h2>
<h4>Manual developments</h4>
<ul>
<li><a href="https://github.com/rafoo/dklib">Dklib</a> is a library defining basic data structures.</li>
<li><a href="http://sigmaid.gforge.inria.fr/">Sigmaid</a> (SIGMA-calculus In Dedukti) is an encoding of the simply-typed ς-calculus in Dedukti.</li>
<li><a href="https://github.com/Deducteam/Libraries">Libraries</a> A github repository that aims to contain every hand-written Dedukti files. In the short run, the two links above should be outdated.</li>
</ul>
<h4>Generated libraries</h4>
<p>Each tarball contains a Makefile in order to check the library. You may want to modify the variables DKDEP and DKCHECK that are the paths of the corresponding binaries.</p>
<ul>
<li><a href="data/libraries/holide.tar.gz">The Holide library</a> is the library produced by Holide on the standard library of the
common format for HOL proof assistant: OpenTheory</li>
<li><a href="data/libraries/matita.tar.gz">The Matita arithmetic library</a> is a library of Dedukti files generated by Krajono.</li>
<li><a href="data/libraries/focalide.tar.gz">The Focalide library</a> is a library of Dedukti files generated by Focalide.</li>
<li><a href="http://deducteam.gforge.inria.fr/lib/zenon_modulo.tar">The Zenon Modulo Set Theory library</a> is a library of Dedukti files generated by Zenon
Modulo and dealing with the B Method set theory. (Remark: this is
a tar archive containing gzipped Dedukti files.)</li>
<li><a href="http://deducteam.gforge.inria.fr/lib/iProverModulo_Dedukti_library.tar">The iProverModulo TPTP library</a> is a library of Dedukti files generated by iProverModulo
from <a href="http://www.cs.miami.edu/~tptp/">TPTP</a> problems. (Remark: this is
a tar archive containing gzipped Dedukti files.)</li>
<li><a href="data/libraries/verine.tar.gz">Verine</a> is a library of Dedukti proofs translated from the SMT solver veriT (work in
progress).</li>
<li><a href="data/libraries/sttforall.tar.gz">STTforall</a> is a library of Dedukti proofs encoded in an extension of Simple Type Theory with prenex polymorphism. These files have been generated from the Matita library encoded in Dedukti.</li>
<li><a href="data/libraries/geocoq.tar.gz">GeoCoqInE</a> is a library of Dedukti proofs encoded in an extension of the Calculus of Inductive Constructions.
It has been generated from the <a href="https://geocoq.github.io/GeoCoq/">GeoCoq</a> library originally written in the <a href="https://coq.inria.fr">Coq</a> theorem prover.</li>
</ul>
<h2>Translators to Dedukti</h2>
<ul>
<li><a href="http://deducteam.gforge.inria.fr/holide/">Holide</a> (HOL In DEdukti) produces Dedukti proofs from HOL proofs, using the <a href="http://www.gilith.com/research/opentheory/">Open Theory</a> standard. </li>
<li><a href="http://deducteam.gforge.inria.fr/krajono/">Krajono</a> ("Pencil" in Esperanto) produces Dedukti files from Matita proofs.</li>
<li><a href="http://deducteam.gforge.inria.fr/focalide/">Focalide</a> (FoCaLize In DEdukti) produces Dedukti files from FoCaLize developments.</li>
<li><a href="http://deducteam.gforge.inria.fr/zenonmodulo/">Zenon Modulo</a> an extension of the tableaux automated theorem prover Zenon with typing and deduction modulo producing Dedukti files.</li>
<li><a href="https://github.com/gburel/iProverModulo">iProverModulo</a> an extension of the resolution automated theorem prover iProver with deduction modulo producing Dedukti files.</li>
<li><a href="http://www.ensiie.fr/~guillaume.burel/blackandwhite_coqInE.html.en">CoqInE</a> (Coq In dEdukti) produces Dedukti proofs from Coq proofs (work in progress).</li>
<li><a href="http://github.com/Deducteam/ekstrakto">Ekstrakto</a> ("To extract" in Esperanto) A tool to extract TPTP problems from a TSTP trace and reconstruct the proof in Dedukti.</li>
</ul>
<h2>Publications</h2>
<p><a href="https://hal.inria.fr/search/index/?qa%5Btext_fulltext%5D%5B%5D=Dedukti&submit_advanced=Rechercher&sort=producedDate_tdate+desc&rows=100">Publications related to Dedukti</a></p>
<p>For an introduction to Dedukti, see this <a href="https://arxiv.org/abs/2311.07185">paper</a> (<a href="data/expressing_examples.tar.gz">examples</a> used in the paper).</p>
<p>Most theories encoded in Dedukti are presented in <a href="https://lmcs.episciences.org/10959/pdf">A Modular Construction of Type Theories.</a></p>
<!--ul>
<li>Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard,
<a href = "http://www.lsv.ens-cachan.fr/~dowek/Publi/expressing.pdf">Expressing Theories in the lambda-Pi-Calculus Modulo Theory and in the Dedukti System</a>,
and the corresponding <a href="data/expressing_examples.tar.gz">examples</a>.</li>
<li>Guillaume Burel, <a href="data/jfla2017/index.html">Exprimer ses théories en Dedukti, le vérificateur de preuves universel</a> JFLA, 2017.</li>
<li>Ronan Saillard, <a href="http://www.cri.ensmp.fr/people/saillard/Files/thesis.pdf">Typechecking in the Lambda-Pi Calculus Modulo: Theory and Practice.</a> Doctoral thesis, 2015.</li>
<li>Ali Assaf, <a href="https://hal.inria.fr/tel-01235303">A framework for defining computational higher-order logics.</a> Doctoral thesis, 2015.</li>
<li>Ali Assaf, <a href="https://hal.inria.fr/hal-01084165">Conservativity of embeddings in the lambda-Pi calculus modulo rewriting.</a> TLCA, 2015.</li>
<li>Ali Assaf and Guillaume Burel, <a href="https://hal.inria.fr/hal-01097412">Translating HOL to Dedukti.</a> PxTP, 2015.</li>
<li>Ali Assaf and Raphaël Cauderlier, <a href="http://eptcs.web.cse.unsw.edu.au/paper.cgi?PxTP2015.9">Mixing HOL and Coq in Dedukti.</a> PxTP, 2015.</li>
<li>Raphaël Cauderlier and Pierre Halmagrand, <a href="https://hal.archives-ouvertes.fr/hal-01171360">Checking Zenon Modulo Proofs in Dedukti.</a> PxTP, 2015.</li>
<li>Ali Assaf, <a href="https://hal.inria.fr/hal-01097401">A calculus of constructions with explicit subtyping.</a> Types, 2014.</li>
<li>Raphaël Cauderlier and Catherine Dubois, <a href="http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=5491">Objects and subtyping in the Lambda-Pi-calculus modulo.</a> Types, 2014.</li>
<li>Ronan Saillard, <a href="data/poster_Ronan.pdf">Dedukti un vérificateur de preuves universel.</a> Poster, 2014.</li>
<li>Ali Assaf, Raphaël Cauderlier, and Ronan Saillard, <a href="data/poster_Ali_Raphael_Ronan.pdf">Dedukti un vérificateur de preuves universel.</a> Poster, 2013.</li>
<li>Ronan Saillard, <a href="http://hal.inria.fr/docs/00/92/99/12/PDF/article.pdf">Towards explicit rewrite rules in the lambda-Pi calculus modulo.</a> IWIL, 2013.</li>
<li>Guillaume Burel, <a href="http://www.easychair.org/publications/?page=90156058">A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo.</a> PxTP, 2013.</li>
<li>Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant, <a href="http://ceur-ws.org/Vol-878/paper2.pdf">The lambda-Pi-calculus Modulo as a Universal Proof Language.</a> PxTP, 2012.</li>
<li>Mathieu Boespflug and Guillaume Burel, <a href="http://ceur-ws.org/Vol-878/paper3.pdf">CoqInE: Translating the Calculus of Inductive Constructions into the lambda-Pi-calculus Modulo.</a> PxTP, 2012.</li>
<li>Quentin Carbonneaux, <a href="http://www.cs.yale.edu/homes/qcar/data/rapport-master.pdf">Compilation jit des termes de preuve.</a> Master thesis, 2012.</li>
<li>Mathieu Boespflug, <a href="https://hal.inria.fr/tel-00672699">Conception d’un noyau de vérification de preuves pour le lambda-Pi-calcul modulo.</a> Doctoral thesis, 2011.</li>
<li>Denis Cousineau and Gilles Dowek, <a href="http://www.lsv.ens-cachan.fr/~dowek/Publi/pts.pdf">Embedding pure type systems in the lambda-pi-calculus modulo.</a> TLCA, 2007.</li>
</ul-->
</div>
<div id="footer">
<a href="https://www.mines-paristech.fr"><img src="img/logo_mines.png" alt="MINES ParisTech" width="100"/></a>
<a href="https://www.inria.fr"><img src="img/logo_inria.png" alt="Inria" width="200"/></a>
<a href="http://deducteam.gforge.inria.fr"><img src="img/logo_deducteam.svg" alt="Deducteam" width="250"/></a>
</div>
</body>
</html>