Tableaux.Prelude.All

• Prelude.Core: everything defined in the prelude, including instances.

Tableaux.Prelude.Atoms

• Prelude.Atoms: the types that are suitable to make free variables
  • The typeclass of atoms

Tableaux.Prelude.AtomInstances

Tableaux.Prelude.Classes

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

Tableaux.Prelude.Core

• Prelude.Core: everything defined in the prelude except instances.

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
  • Tactics
  • Rocq's default behaviour

Tableaux.Prelude.Sets

• Prelude.Sets: an effective axiomatization of sets
  • Axiomatization of sets as a typeclass

Tableaux.Prelude.SetInstances

• Prelude.SetInstances: Instances of the set typeclasses for nat and strings

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.ProofInstance

Tableaux.Semantics

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

Tableaux.Skolemization

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

Tableaux.SkolemizationInstances

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

Tableaux.SyntaxInstance

• SyntaxInstance: instantiation of the atoms using strings

Tableaux.Extraction

• • Extraction for constants and basic inductives
  • Syntax
  • Checking
  • Extraction

drinker

branching