| Utilities for reasonning | |
|---|---|
| replace.v | |
| classical_help.v | |
| Utilities for lists | |
| list_fall_exst.v | |
| list_in_t.v | |
| list_fall_exst_t.v | |
| 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 Equivalences (PME) | |
| 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 equivalences, pme closure |
| Syntax and semantics of Boolean BI | |
| formula.v | the syntax of BBI |
| css.v | the tableaux branches for BBI |
| kripke.v | the PME semantics for BBI |
| Semantic Tableaux proofs for Boolean BI | |
| bbi_expansion.v | BBI tableaux expansion definition |
| bbi_exp_props.v | properties of BBI tableaux expansion |
| bbi_closed_branch.v | closure for branches in BBI tableaux |
| bbi_tableaux.v | properties of BBI tableaux |
| The soundness of Tableaux proofs | |
| bbi_realizability.v | realizable branches have no closed tableaux |
| The strong completeness of Tableaux proofs | |
| bbi_strategy.v | infinite enumeration for BBI tableaux statements |
| bbi_oracle.v | the counter-model building oracle |
| bbi_simple.v | simple PMEs |
| bbi_basic.v | basic PMEs |
| bbi_sequence.v | the tool to build an increasing sequence of branches |
| bbi_limit.v | the BBI tableaux extracted counter-model |
| bbi_hintikka.v | Hintikka built counter-models |
| The Main Theorems | |
| bbi_sound_and_complete.v | |