Main Page Index Table of Contents
  • K* in Coq
    • Inductive Characterizations
    • Formulas
    • Models
  • Hilbert System
    • Soundness
    • Equivalence to Segerberg style Hilbert system
    • Soundness for Finite Models
  • Clauses and Support
    • Signed Formulas
    • Clauses and Support
    • Request
    • Subformula Closure
    • Associtated Formuals
  • Demos
    • Model Existence
    • Pruning
    • Refutation Predicates and corefutability of the pruning demo
    • Refutation Correctness
  • Hilbert Refutations
    • Completeness
    • Small Model Theorem
  • History-based Gentzen system for K*
    • Soundness for Finite Models
    • Refutation Predicates and corefutability of the pruning demo
    • Refutation Completeness for History-Free Clauses
  • Main Results
Generated by coqdoc and improved with CoqdocJS