Repository of logic definitions for Lambdapi
-
TFF: polymorphic first-order logic (with a few definitions and theorems on natural numbers and polymorphic lists)
-
U: theory introduced in Axioms for Mathematics
-
Zenon: logic files used by the automated theorem prover ZenonModulo
-
PTS: Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo