This

It is distributed under the

- Classical
- Arith, Peano_dec, MinMax, Omega
- List, Permutation

The Makefile was generated by the

The

Here is a short description of the different modules

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 |

The TYPES team

CNRS, Bâtiment LORIA, BP 239

54506 Vandoeuvre-lès-Nancy

France

Last modification :