| Utilities for reasonning | |
|---|---|
| replace.v | |
| classical_help.v | |
| Utilities for (dependent) lists and parametric terms | |
| list_fall_exst.v | |
| list_in_t.v | |
| list_fall_exst_t.v | |
| dlist.v | length dependent lists |
| term.v | terms based on a signature |
| Utilities for predicates (viewed as sets) and maps | |
| predicate.v | sets, inclusion, (extensional) identity, [binary|indexed] unions & intersections, pred_solve tactic |
| maps.v | maps, injectivivity, (infinite) surjectivity, boundedness, direct and inverse images |
| Utilities for finite sets | |
| carrier.v | lists as carriers of finite sets/predicates |
| finite.v | properties of finite sets |
| Utilities for graphs of functions | |
| graph.v | graphs of functions |
| uniq_choice.v | a unique choice recursive principle |
| Utilities for closure operators and systems of rules | |
| closure.v | properties of closure operators |
| system.v | relations defined by systems of finitary derivation rules, proof objects |
| system_extensions.v | extra properties of rule systems, compactness property |
| Utilities for natural numbers and indexations by the type nat | |
| natpred.v | sets of natural numbers |
| natseq.v | sequences of natural numbers |
| maxf.v | the maximum function on sequences of nat |
| cantorbernstein.v | a constructive proof for indexing types by nat |
| enum.v | (surjective) enumerations by nat |
| nat2.v | a bijection nat <-> nat*nat |
| enumerations.v | enumerations and recursive datatypes |
| nathole.v | an injection nat -> nat avoiding a finite set of elements |
| Utilities for analytic tableaux | |
| branch.v | generic branch equivalence |
| tableaux.v | generic tableaux proofs and properties of tableaux proofs |
| Main data structures for Partial Monoidal Orders (PMO) | |
| labels.v | a particular nat indexed set of letters |
| words.v | words (as list of letters), permutation equivalence, substitutions |
| constraints.v | constraints (pairs of words), languages and alphabets |
| substitutions.v | substitutions based on words of labels |
| pme.v | partial monoidal orders, pmo closure |
| Syntax and semantics of BI | |
| formula.v | the syntax of BI |
| css.v | the tableaux branches for BI |
| kripke.v | the PMO semantics for BI |
| Semantic Tableaux proofs for BI | |
| bi_expansion.v | BI tableaux expansion definition |
| bi_exp_props.v | properties of BI tableaux expansion |
| bi_closed_branch.v | closure for branches in BI tableaux |
| bi_tableaux.v | properties of BI tableaux |
| The soundness of Tableaux proofs | |
| bi_realizability.v | realizable branches have no closed tableaux |
| The strong completeness of Tableaux proofs | |
| bi_strategy.v | infinite enumeration for BI tableaux statements |
| bi_oracle.v | the counter-model building oracle |
| bi_simple.v | simple PMOs |
| bi_basic.v | basic PMOs |
| bi_sequence.v | the tool to build an increasing sequence of branches |
| bi_limit.v | the BOI tableaux extracted counter-model |
| bi_hintikka.v | Hintikka built counter-models |
| The Main Theorems | |
| bi_sound_and_complete.v | |