Fix the solvers to formally use modus ponens/tollens to solve the program rather than our best guess Given: $P \implies Q$ Tollens: $\neg Q \therefore \neg P$ Ponens: $P \therefore Q$ where $Q = D_1 \vee D_2 \vee D_3 \vee \dots$
Fix the solvers to formally use modus ponens/tollens to solve the program rather than our best guess
Given:
$P \implies Q$
$\neg Q \therefore \neg P$
$P \therefore Q$
Tollens:
Ponens:
where$Q = D_1 \vee D_2 \vee D_3 \vee \dots$