Tableaux.Prelude.All

• Prelude.All: get everything defined in the prelude.

Tableaux.Prelude.Atoms

• Prelude.Atoms: the types that are suitable to make free variables
  • The typeclass of atoms
  • Some usual instantiations, hidden under an importable module.

Tableaux.Prelude.Classes

• Prelude.Classes: definition of common typeclasses
  • Typeclasses definition
  • Equivalence
  • Common instances
  • Generic instances
  • Monads

Tableaux.Prelude.Ind

• Prelude.Ind: useful inductives not defined in Corelib/Stdlib
  • Inductives
  • Equivalence between Forall and In.
  • Some properties of Forall

Tableaux.Prelude.Init

• Prelude.Init: set basic flags and Corelib/Stdlib exports
  • Rocq's default behaviour

Tableaux.Prelude.Sets

• Prelude.Sets: an effective axiomatization of sets and some instances
  • Axiomatization of sets as a typeclass
  • Built-in instances

Tableaux.Prelude.Utils

• Prelude.Utils: some utility functions / lemmas

Tableaux.Prelude.LocallyNamelessClasses

• Prelude.LocallyNamelessClasses: classes for locally nameless representation
  • Variable opening: replacing a bound variable with an atom
  • Variable substitution: replacing a free variable with something
  • Further free instances of BV.
  • Further free instances of Subst.
  • Free variable and free-variable closedness
  • Further free instances of FV.

Tableaux.All

Tableaux.Checker

• Checker: sound algorithm to check a tableau proof
  • 1. The algorithm
  • 2. Soundness
  • 3. Extended Syntax
  • 4. The tableaux tactic

Tableaux.Core

Tableaux.ExtendedSyntax

• ExtendedSyntax: full first-order logic syntax
  • 1. Extended syntax
  • 2. Extended semantics
  • 3. Syntax translation
  • 4. Correspondance of the semantics
  • 5. Helper to transform substitution into internal substitution
  • 6. Notation system for the extended syntax

Tableaux.Proofs

• Proofs: definition of free-variable tableaux proofs.
  • Tableaux
  • Expansion rules
  • Soundness

Tableaux.Semantics

• Semantics: semantics of first-order logic.
  • Replacement model

Tableaux.Skolemization

• Skolemization: a generic class for Skolemization
  • Some classic instances

Tableaux.Syntax

• Syntax: definition of a locally-nameless first-order logic syntax.
  • First-order logic terms
  • Subterms
  • Minimal first-order logic formulas
  • Utils functions
  • Function symbols
  • Concrete instances

drinker

branching