This archive contains the final version 2.0 of

It is distributed under the

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

The Makefile was generated by the

This code is direct adaptation of the formal proof of strong completeness of partial monoidal Boolean BI, available elsewhere on this site: you can find an informal proof there as well.

Here is a short description of the different modules

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 |

The TYPES team

CNRS, Bâtiment LORIA, BP 239

54506 Vandoeuvre-lès-Nancy

France

Last modification :