search

LucianoXu / NQPV

NQPV is an assistant tool for the formal verification of nondeterministic quantum programs.
Apache License 2.0
4 stars 0 forks source link

More backward strategy (with Union) #47

Closed LucianoXu closed 2 years ago

LucianoXu commented 2 years ago

We can implement the strategy of always using union to divide predicate sets. The strategy here resembles the 'tactics' used in Lean, which refers to a bunch of specified proving attempts.

LucianoXu commented 2 years ago

Actually we can see from the definition of weakest preconditions that union rules should be applied first.