Main Page Index Table of Contents
  • K in Coq
    • Formulas
    • Models
  • Hilbert System
    • Soundness
    • Finite Models
  • Signed Formulas, Clauses, and Support
    • Signed Formulas
    • Clauses and Support
    • Request
    • Subformula Closure
    • Size of Subformula Universes
  • Demos
    • Model Existence
    • Pruning
    • Refutation Predicates and corefutability of the pruning demo
    • Refutation Completeness
  • Hilbert Refutations
    • Completeness
    • Small Model Theorem
    • Canonicity of pruning demo
  • Gentzen System for K
    • Refutation Completeness
  • Construction of a Universal Model
  • Main Results
Generated by coqdoc and improved with CoqdocJS