Project Page Index Table of Contents

testfree-PDL.testfree_PDL_def
  • Test-free PDL in Coq
  • Formulas
    • Models
    • Soundness for Finite Models
  • Clauses and Hintikka Sets
    • Signed Formulas
    • Subformula Closure
    • Hintikka Sets
    • Request
    • Associated Formuals

testfree-PDL.demo
  • Demos
    • Model Existence
    • Pruning
    • Refutation Predicates and corefutability of the pruning demo
    • Refutation Correctness

testfree-PDL.hilbert_ref
  • Hilbert Refutations
    • Completeness
    • Small Model Theorem
Generated by coqdoc and improved with CoqdocJS