Vct.Assumptions

Vct.Atom

Vct.BoxClause

Vct.Cnf

Vct.CplClause

Vct.CplSolution

Vct.CplSolver

• Axioms

Vct.DiaClause

Vct.Extract

Vct.Fml

Vct.ImportStd

Vct.Kripke

Vct.Lclauses

Vct.ListExt

Vct.Lit

• Equality lemmas
• Forcing

Vct.Mcnf

Vct.Mcnf.Conversion

• Conversion correctness

Vct.Mcnf.Mcnf

• Helpers
• Extensions

Vct.Mcnf.Simplification

• Simplifications

Vct.Nnf

Vct.Nnfl

Vct.Solver

Vct.Solver.Cached

• Equivalence to NoWit

Vct.Solver.Cct

Vct.Solver.Completeness

Vct.Solver.FiredBoxes

Vct.Solver.Kt

• Soundness

Vct.Solver.McnfExt

• Conflict set lemmas

Vct.Solver.NoWit

Vct.Solver.SearchBasics

• Measurement

Vct.Solver.Soundness

• Cct.wf proofs
• Soundness
  • Resolution
  • Soundness of cct
  • Soundness of tableau

Vct.Solver.Spec

Vct.Solver.TailRec

Vct.Tactics

• • Find and destruct matches

Vct.Tree

Vct.Trie

Vct.Valuation