Verification with GDV

Structural Verification

• Existing Checks:
  Unique names; Parents exist; Acyclic; false roots for refutations; Independence of splits
• New Checks for Assumptions
  • Propagation from parents to inferred formula assumptions([...]) list
  • Discharged assumptions may be removed (optional but normal)
  • All assumptions discharged eventually
• Uniqueness of new symbols in leaves introducing them (Henkin axioms)

Semantic Verification

• Use trusted ATP to verify inferences
• Existing Checks:
  Leaves from problem; Leaf tautologies; Logical consequences; Satisfiability preserving steps
• New Checks for Assumptions
  • Discharged assumptions as preconditions on parents
  • Decomposed into finer grained steps for verification