Skip to content

Commit 5fb3059

Browse files
committed
make inc induction slide more clear.
1 parent fab0d00 commit 5fb3059

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

doc/slides/present.pdf

-136 Bytes
Binary file not shown.

doc/slides/present.tex

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -125,13 +125,13 @@ \subsection{Focus on Proofs}
125125
Given $A$, find $P$:
126126
\begin{align*}
127127
I & \implies & P\\
128-
P & \implies & \neg B\\
128+
P & \implies & \neg b\\
129129
A \wedge P \wedge T & \implies & P'
130130
\end{align*}
131131
Then update $A \leftarrow A \wedge P$.
132132

133133
In PDR/IC3, $A$ is CNF, $P$ is a clause which blocks
134-
states than can reach $B$.
134+
states than can reach $B$, indicated above as $b$.
135135
\end{columns}
136136
\end{frame}
137137

0 commit comments

Comments
 (0)