The theory of a theorem is the set of constants, axioms, and definitions needed to prove this theorem. It contains also the definitions that appear in the statement of axioms. This notion of theory is extended in a natural way to the other kind of objects.
The main dependencies of a theorem are the constants, axioms, definitions, and lemmas that are used in its proof that do not appear in the transitive closure of dependencies of that theorem.
A constant is a symbol that does not have a definition. In general, such symbol comes with axioms that define its meaning.
A Type Operator is a type constant, such as the type "nat" of natural numbers. It has no definition.
Logipedia does not use the notion of inductive types nor recursive function. Hence, inductive types and recursive functions are axiomatized.
We suppose that, as the user of the target system, you already know how to build a generic Makefile to compile the files.
If you want to add your system on Logipedia, we invite you to contact Gilles Dowek and François Thiré.
Logipedia is an encyclopedia of proofs expressed in any theory defined in Dedukti. Currently, all proofs are expressed in the same theory: STTForall. If you want add more STTForall proofs or define a new logic in Dedukti, contact Gilles Dowek and François Thiré.
Logipedia is an open source project. You can find us on GitHub.