ICL.Base
- Base Library for ICL
- De Morgan laws
- Size recursion
- Iteration
- Decidability
- Lists
- Decidability laws for lists
- Membership
- Disjointness
- Inclusion
- Setoid rewriting with list inclusion and list equivalence
- Equivalence
- Filter
- Element removal
- Cardinality
- Duplicate-free lists
- Power lists
- Finite closure iteration
- Deprecated names, defined for backward compatibilitly
ICL.PropL
- Formulas and contexts
- Assignments and Satisfaction
- Generic Entailment Relations
- Intuitionistic system
- Classical system
- Glivenko's theorem
- Intuitionistic Hilbert system
ICL.ctab
- Boolean satisfaction
- Validity and boolean entailment
- Signed formulas and clauses
- Solved Clauses
- Refutation predicates
- Decision trees
- Refutation lemma
- Decidability of classical ND entailment
- Agreement of classical ND entailment with boolean entailment