Skip to content

Commit 2619c56

Browse files
seanmclseanmcl
committed
misc
1 parent bfe4bb2 commit 2619c56

14 files changed

+618
-297
lines changed

‎.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -19,3 +19,5 @@
1919
*~
2020
.cm
2121
_region_.tex
22+
*.fdb_latexmk
23+
*.fls

‎abstract.tex

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
2+
\begin{abstract}
3+
Non-classical logics provide a flexible means for describing and
4+
reasoning about diverse computational phenomena.
5+
\emph{Intuitionistic logic} provides a foundation for constructive
6+
mathematics and is the
7+
basis of numerous logical frameworks and proof assistants which are
8+
used to reason about programs. \emph{Modal logics} permit succinct
9+
reasoning about possible worlds, which has applications to
10+
authorization and distributed computing. \emph{Linear logic} and
11+
\emph{ordered logic}, with their interpretation of hypotheses as
12+
resources, are used to study stateful and concurrent systems.
13+
14+
Theorem proving in these logics is typically difficult. For example,
15+
while in classical logic the decision problem for the propositional
16+
fragment is NP-complete, intuitionisitic logic is PSPACE-complete,
17+
while even fragments of propositional linear logic are undecidable.
18+
Nevertheless, it is fundamental to the adoption of such expressive
19+
logics that we develop practical theorem proving tools.
20+
21+
We describe a general method for building efficient theorem provers for
22+
non-classical logics called the \emph{polarized inverse method}. The
23+
\emph{generality} of our approach comes from the use of the inverse method, a
24+
well-known proof search strategy for cut-free sequent calculi, and the use of
25+
\emph{constraints} for delaying the results of costly computations.
26+
\emph{Efficiency} comes from the relatively novel proof-theoretic methods of
27+
\emph{focusing} and \emph{polarization} as well as more standard techniques
28+
such as redundancy elimination.
29+
30+
Throughout the thesis we will demonstrate by example that the inverse
31+
method, augmented with constraints, focusing, and polarization, forms
32+
a strong foundation for efficient theorem proving in non-classical
33+
logics. We give support to our claims by describing an implementation of
34+
a theorem prover called \emph{Imogen} for propositional and first-order logic,
35+
first-order logic with equality, some first-order some standard
36+
intuitionistic modal logics (K, T, K4, S4, S5), lax logic,
37+
Pfenning and Davies' computational modal logic, linear and ordered
38+
logic).
39+
We find in empirical tests
40+
that Imogen compares favorably with existing implementations. For
41+
first-order logic with equality, ordered logic and some modal logics,
42+
Imogen is the first and only existing implementations.
43+
\end{abstract}
44+
45+
%%% Local Variables:
46+
%%% mode: latex
47+
%%% TeX-master: "thesis"
48+
%%% End:

‎chapter-prop.tex

+281-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,285 @@
11
\chapter{Prop}
22
\label{chapter-prop}
33

4+
\newcommand{\Ps}{P(\vec{s}\,)}
5+
\newcommand{\Pt}{P(\vec{t}\;)}
6+
\newcommand{\Pu}{P(\vec{u}\,)}
7+
\newcommand{\Pv}{P(\vec{v}\,)}
48

5-
Prop!\cite{cervesato13substructural}
9+
\begin{figure}
10+
\footnotesize
11+
\[
12+
\arraycolsep=15pt
13+
\begin{array}{c}
14+
\begin{array}{ccc}
15+
\infer[\mbox{E-R}]{\CSeq{\Phi}{\Gamma}{E}}{\Phi \models E}
16+
&
17+
\infer[\mbox{E-L}]{\CSeq{\Phi}{\Gamma, E}{C}}{\CSeq{\Phi \And E}{\Gamma}{C}}
18+
&
19+
\infer[\mbox{E-init}]{\CSeq{\Phi}{\Gamma, \Ps)}{\Pt}}{\Phi \models \vec{s} \EEq \vec{t}}
20+
\end{array}
21+
\\[2em]
22+
23+
\begin{array}{cc}
24+
\infer[\Top$-R$]{\CSeq{\Phi}{\Gamma}{\Top}}{}
25+
&
26+
\mbox{No rule for $\Top$-L}
27+
\end{array}
28+
\\[2em]
29+
30+
\begin{array}{cc}
31+
\mbox{No rule for $\Bot$-R}
32+
&
33+
\infer[\Bot$-L$]{\CSeq{\Phi}{\Gamma, \Bot}{C}}{}
34+
\end{array}
35+
\\[2em]
36+
37+
\begin{array}{cc}
38+
\infer[\And$-R$]{\CSeq{\Phi}{\Gamma}{A \And B}}{\CSeq{\Phi}{\Gamma}{A} & \CSeq{\Phi}{\Gamma}{B}}
39+
&
40+
\infer[\And$-L$]{\CSeq{\Phi}{\Gamma, A \And B}{C}}{\CSeq{\Phi}{\Gamma, A, B}{C}}
41+
\end{array}
42+
\\[2em]
43+
44+
\begin{array}{ccc}
45+
\infer[\Or$-R$_1]{\CSeq{\Phi}{\Gamma}{A \Or B}}{\CSeq{\Phi}{\Gamma}{A}}
46+
&
47+
\infer[\Or$-R$_2]{\CSeq{\Phi}{\Gamma}{A \Or B}}{\CSeq{\Phi}{\Gamma}{B}}
48+
&
49+
\infer[\Or$-L$]{\CSeq{\Phi}{\Gamma, A \Or B}{C}}{\CSeq{\Phi}{\Gamma, A}{C} & \CSeq{\Phi}{\Gamma, B}{C}}
50+
\end{array}
51+
\\[2em]
52+
53+
\begin{array}{cc}
54+
\infer[\Imp$-R$]{\CSeq{\Phi}{\Gamma}{A \Imp B}}{\CSeq{\Phi}{\Gamma, A}{B}}
55+
&
56+
\infer[\Imp$-L$]{\CSeq{\Phi}{\Gamma, A \Imp B}{C}}{\CSeq{\Phi}{\Gamma, B}{C} & \CSeq{\Phi}{\Gamma, A \Imp B}{A}}
57+
\end{array}
58+
\\[2em]
59+
60+
\begin{array}{cc}
61+
\infer[\All$-R$]{\CSeq{\Phi}{\Gamma}{\All x.~A(x)}}{\CSeq{\Phi}{\Gamma}{A(a)} & a\not\in\Phi, \Gamma, A}
62+
&
63+
\infer[\All$-L$]{\CSeq{\Phi}{\Gamma, \All x.~A(x)}{C}}{\CSeq{\Phi}{\Gamma, \All x.~A(x), A(t)}{C}}
64+
\end{array}
65+
\\[2em]
66+
67+
\begin{array}{cc}
68+
\infer[\Ex$-R$]{\CSeq{\Phi}{\Gamma}{\Ex x.~A(x)}}{\CSeq{\Phi}{\Gamma}{A(t)}}
69+
&
70+
\infer[\Ex$-L$]{\CSeq{\Phi}{\Gamma, \Ex x.~A(x)}{C}}{\CSeq{\Phi}{\Gamma, A(a)}{C} & a\not\in\Phi, \Gamma, A}
71+
\end{array}
72+
\\[2em]
73+
74+
\end{array}
75+
\]
76+
\caption{The backward constraint calculus, \C.}
77+
\label{fig:backward}
78+
\end{figure}
79+
80+
\begin{figure}
81+
\[
82+
\arraycolsep=15pt
83+
\begin{array}{c}
84+
\begin{array}{cc}
85+
\infer[\mbox{id}]{\Phi \models \Phi}{}
86+
&
87+
\infer[\mbox{trans}]{\Phi_1 \models \Phi_3}{\Phi_1\models\Phi_2 & \Phi_2\models\Phi_3}
88+
\end{array}
89+
\\[2em]
90+
\begin{array}{ccc}
91+
\infer[\And_1]{\Phi_1 \And \Phi_2 \models \Phi_1}{}
92+
&
93+
\infer[\And_2]{\Phi_1 \And \Phi_2 \models \Phi_2}{}
94+
&
95+
\infer[\And]{\Phi \models \Phi_1 \And \Phi_2}{\Phi \models \Phi_1 & \Phi \models \Phi_2}
96+
\end{array}
97+
\\[2em]
98+
\begin{array}{ccc}
99+
\infer[$refl$]{\Phi \models t\EEq t}{}
100+
&
101+
\infer[$sym$]{\Phi \models s\EEq t}{\Phi\models t\EEq s}
102+
&
103+
\infer[$vec$]{\Phi \models \vec{s}\EEq \vec{t}}{|s| = |t| = n & \Phi\models s_1\EEq t_1 & \cdots & \Phi\models s_n\EEq t_n}
104+
\end{array}
105+
\\[2em]
106+
\end{array}
107+
\]
108+
\caption{Properties of the entailment relation.}
109+
\label{fig:entailment}
110+
\end{figure}
111+
112+
To verify the internal integrity (soundness and completeness) of $\C$, we prove the standard
113+
cut elimination and identity properties.
114+
115+
\begin{theorem}[Identity] For any $\Phi, \Gamma, A$, \[\CSeq{\Phi}{\Gamma, A}{A}\].\end{theorem}
116+
\begin{proof}
117+
Induction on $A$. Most cases are simple uses of the induction hypotheses. We
118+
show some representative cases.
119+
\begin{description}
120+
\item[Case] $A = E$. By entailment rules id and $\And_2$, we have $\Phi\And E\models E$.
121+
Therefore
122+
\[
123+
\infer[$E-L$]{\CSeq{\Phi}{\Gamma, E}{E}}{\infer[$E-R$]{\CSeq{\Phi\And E}{\Gamma}{E}}{\Phi\And E \models E}}
124+
\]
125+
126+
\item[Case] $A = \Ps$. By entailment rules refl and vec, we have $\Phi\models \vec{s}\EEq\vec{s}$.
127+
Therefore
128+
\[
129+
\infer[$init$]{\CSeq{\Phi}{\Gamma, \Ps}{\Ps}}{\Phi\models\vec{s}\EEq\vec{s}}
130+
\]
131+
132+
\item[Case] $A = \All x.~B(x)$
133+
\[
134+
\infer[\All$-R$]{\CSeq{\Phi}{\Gamma, \All x.~B(x)}{\All x.~B(x)}}{\infer[\All$-L$]{\CSeq{\Phi}{\Gamma, \All x.~B(x)}{B(a)}}{\deduce{\CSeq{\Phi}{\Gamma, \All x.~B(x), B(a)}{B(a)}}{\D'}}}
135+
\]
136+
137+
where $\D'$ exists by induction hypothesis.
138+
\end{description}
139+
\end{proof}
140+
141+
\begin{theorem}[Admissibility of Cut]\label{thm:cut-admissible}
142+
The following rule is admissible:
143+
144+
\[
145+
\infer-[cut]{\CSeq{\Phi}{\Gamma}{C}}{\CSeq{\Phi}{\Gamma}{A} & \CSeq{\Phi}{\Gamma, A}{C}}
146+
\]
147+
\end{theorem}
148+
149+
Following Pfenning~\cite{pfenning95lics,pfenning00ic}, we use a structural cut elimination
150+
argument. The proof requires the following lemmas describing some properties of the
151+
entailment relation\footnote{Indeed, the proof of cut elimination largely determined the
152+
minimal requirements of the entailment relation.}.
153+
154+
\begin{lemma}[Constraint Weakening]\label{lem:e-weaken}
155+
For any $\Phi, \Phi', \Gamma, C$, if $\Phi'\models \Phi$ and $\CSeq{\Phi}{\Gamma}{C}$
156+
then $\CSeq{\Phi'}{\Gamma}{C}$.
157+
\end{lemma}
158+
\begin{proof}
159+
By induction on the derivation $\CSeq{\Phi}{\Gamma}{C}$. Some cases:
160+
\begin{description}
161+
\item[Case]
162+
\[\infer[$E-R$]{\CSeq{\Phi}{\Gamma}{E}}{\Phi\models E}\]
163+
By transitivity of entailment (rule trans) we have $\Phi'\models E$ so
164+
$\CSeq{\Phi'}{\Gamma}{E}$ by rule E-R.
165+
\item[Case]
166+
\[\infer[$E-L$]{\CSeq{\Phi}{\Gamma, E}{C}}{\CSeq{\Phi\And E}{\Gamma}{C}}\]
167+
By entailment reasoning, we have $\Phi'\And E\models\Phi\And E$. By induction
168+
hypothesis we have that $\CSeq{\Phi'\And E}{\Gamma}{C}$ so $\CSeq{\Phi'}{\Gamma, E}{C}$
169+
by rule E-L.
170+
\end{description}
171+
\end{proof}
172+
173+
\begin{lemma}[Inversion]\label{lem:e-invert}
174+
For any $\Phi, \Gamma, E, C$ if $\CSeq{\Phi}{\Gamma, E}{C}$ then $\CSeq{\Phi\And E}{\Gamma}{C}$.
175+
\end{lemma}
176+
\begin{proof} Easy induction on the derivation. \end{proof}
177+
178+
\begin{lemma}[Contraction]\label{lem:contract}
179+
If $\CSeq{\Phi}{\Gamma, \Ps, \Pt}{C}$ and $\Phi\models\vec{s}\EEq\vec{t}$ then
180+
$\CSeq{\Phi}{\Gamma, \Ps}{C}$.
181+
\end{lemma}
182+
183+
\begin{proof}
184+
Induction on the derivation $\D$ of $\CSeq{\Phi}{\Gamma, \Ps, \Pt}{C}$.
185+
\begin{description}
186+
\item[Case] $\D$ is
187+
\[
188+
\infer[\mbox{E-init}]{\CSeq{\Phi}{\Gamma', \Pu}{\Pv}}{\Phi \models \vec{u} \EEq \vec{v}}
189+
\]
190+
We have $C = \Pv$ and $\Gamma, \Ps, \Pt = \Gamma', \Pu$.
191+
If $\vec{u} \neq \vec{t}$ then we already have
192+
$\CSeq{\Phi}{(\Gamma'\setminus \Pt), \Pu}{\Pv}$ by rule E-init. Otherwise
193+
we have $\Gamma' = \Gamma, \Ps$ and $\Phi\models\vec{t} \EEq \vec{v}$ and $\Phi\models\vec{s} \EEq \vec{t}$ so
194+
$\Phi\models\vec{s} \EEq \vec{v}$. Then $\CSeq{\Phi}{\Gamma, \Ps}{\Pv}$
195+
by rule E-init.
196+
\item[Case] $\D$ is
197+
\[
198+
\infer[\mbox{E-L}]{\CSeq{\Phi}{\Gamma, \Ps, \Pt, E}{C}}{\CSeq{\Phi\And E}{\Gamma}{C}}
199+
\]
200+
Since $E$ can not be an atomic formula, $E\neq \Ps$ and, $E\neq \Pt$.
201+
Since $\Phi\models \vec{s}\EEq\vec{t}$, $\Phi\And E\models \vec{s}\EEq\vec{t}$, so
202+
the induction hypothesis applies and we have $\CSeq{\Phi\And E}{\Gamma, \Ps}{C}$.
203+
The result follows from an application of rule E-L.
204+
\end{description}
205+
\end{proof}
206+
207+
\begin{lemma}[Constraint Substitution]\label{lem:subst}
208+
If $\CSeq{\Phi}{\Gamma}{\Ps}$ and $\Phi\models\vec{s}\EEq\vec{t}$ then
209+
$\CSeq{\Phi}{\Gamma}{\Pt}$.
210+
\end{lemma}
211+
212+
\begin{proof}
213+
Induction on the derivation $\D$ of $\CSeq{\Phi}{\Gamma}{\Ps}$.
214+
\begin{description}
215+
\item[Case] $\D$ is
216+
\[
217+
\infer[\mbox{E-init}]{\CSeq{\Phi}{\Gamma', \Pu}{\Pv}}{\Phi \models \vec{u} \EEq \vec{v}}
218+
\]
219+
\end{description}
220+
\end{proof}
221+
222+
223+
\begin{proof}[Proof of Theorem~\ref{thm:cut-admissible}]
224+
Let $\D :: \CSeq{\Phi}{\Gamma}{A}$ and $\E :: \CSeq{\Phi}{\Gamma, A}{C}$.
225+
We proceed by induction on $A, \D, \E$. The majority of the cases don't modify
226+
the constraints in any way, and the cases are identical with Pfenning's proof. We
227+
show the cases where constraints play a significant role.
228+
229+
\begin{description}
230+
\item[Case]
231+
Initial cuts. These are cuts where one of the derivations is initial with A as
232+
its principle formula.
233+
\begin{description}
234+
\item[Case]
235+
$\D$ is \[\infer[$E-R$]{\CSeq{\Phi}{\Gamma}{E}}{\Phi\models E}\]
236+
Since $A = E$ we have $\CSeq{\Phi}{\Gamma, E}{C}$. By inversion (Lemma~\ref{lem:e-invert}) we
237+
have a derivation of $\CSeq{\Phi\And E}{\Gamma}{C}$.
238+
Then since $\Phi\models E$, we have $\Phi\models\Phi\And E$ (constraint rules id and $\And$) so by
239+
constraint weakening (Lemma~\ref{lem:e-weaken}) we have $\CSeq{\Phi}{\Gamma}{C}$ as required.
240+
\item[Case]
241+
$\D$ is \[\infer[$E-init$]{\CSeq{\Phi}{\Gamma', \Ps}{\Pt}}{\Phi\models \vec{s}\EEq\vec{t}}\]
242+
Then $\Gamma = \Gamma', \Ps$, $A = \Pt$. By assumption we
243+
have $\CSeq{\Phi}{\Gamma', \Ps, \Pt}{C}$. By contraction (Lemma~\ref{lem:contract})
244+
we have $\CSeq{\Phi}{\Gamma', \Ps}{C}$ as required.
245+
\item[Case]
246+
$\E$ is \[\infer[$E-init$]{\CSeq{\Phi}{\Gamma, \Ps}{\Pt}}{\Phi\models \vec{s}\EEq\vec{t}}\]
247+
Then $A = \Ps, C = \Pt$. By assumption we
248+
have $\CSeq{\Phi}{\Gamma}{\Ps}$. The result follows by constraint substitution (Lemma~\ref{lem:subst}).
249+
250+
\end{description}
251+
252+
\item[Case]
253+
Principal cuts.
254+
\begin{description}
255+
\item[Case] Foo
256+
\item[Case] Bar
257+
\end{description}
258+
259+
\item[Case]
260+
Left commutative cuts.
261+
\begin{description}
262+
\item[Case] Foo
263+
\item[Case] Bar
264+
\end{description}
265+
266+
\item[Case]
267+
Right commutative cuts.
268+
\begin{description}
269+
\item[Case] Foo
270+
\item[Case] Bar
271+
\end{description}
272+
273+
\end{description}
274+
275+
276+
\end{proof}
277+
278+
Simmons~\cite{simmons14tocl} considerably simplified the proofs of
279+
cut elimination and identity using a technique he calls
280+
\emph{structural focalization}.
281+
282+
%%% Local Variables:
283+
%%% mode: latex
284+
%%% TeX-master: "thesis"
285+
%%% End:

0 commit comments

Comments
 (0)