writing: 385562f7e51bef00ace4a3ca2e8182665e7b95af
1: \iffalse
2: \documentclass[]{article}
3:
4: \usepackage{cite}
5: \usepackage{rotating}
6: \usepackage{hyperref}
7: \usepackage{graphicx}
8: \usepackage{mathtools}
9: \usepackage{amssymb}
10: \usepackage[T1]{fontenc}
11: % \usepackage{enumitem}
12: \usepackage{paralist}
13: \usepackage{csquotes}
14: \usepackage[affil-it]{authblk}
15: \usepackage{listings}
16: \usepackage{fixltx2e}
17: \usepackage[numbers]{natbib}
18: \usepackage{mathpartir}
19: \usepackage{mmm}
20:
21: % Treat paragraph as subsubsubsection
22: \usepackage{titlesec}
23: \setcounter{secnumdepth}{4}
24:
25: \DeclareMathOperator{\md5}{MD5}
26:
27: \newcommand{\blank}{\cdot}
28:
29: \fi
30:
31: \documentclass[runningheads,a4paper]{llncs}
32:
33: \usepackage{amsmath}
34: \usepackage{amssymb}
35: \setcounter{tocdepth}{3}
36: \usepackage{graphicx}
37: \usepackage{minted}
38: \usepackage[caption=false]{subfig}
39:
40: \usepackage{tikz-qtree}
41: \usepackage{tikz}
42: \usetikzlibrary{shapes,arrows,decorations.pathreplacing,calc}
43:
44: \usepackage{algorithm}
45: \usepackage[noend]{algpseudocode}
46:
47: \usepackage{url}
48: \urldef{\mailsa}\path|cmwarburton@dundee.ac.uk, katya@computing.dundee.ac.uk|
49: \newcommand{\keywords}[1]{\par\addvspace\baselineskip
50: \noindent\keywordname\enspace\ignorespaces#1}
51:
52: % Abbreviations
53: \newcommand{\qcheck}{\textsc{QuickCheck}}
54: \newcommand{\qspec}{\textsc{QuickSpec}}
55: \newcommand{\hspec}{\textsc{HipSpec}}
56: \newcommand{\equal}{=}
57: \newcommand{\fc}{System $F_C$}
58:
59: % Semantic markup
60: \providecommand{\coq}[1]{\texttt{#1}}
61: \newenvironment{haskell}{\ttfamily}{\par}
62: \newenvironment{haskellblock}{\begin{minted}{haskell}}{\end{minted}}
63: \newenvironment{coqblock}{\ttfamily}{\par}
64: \newcommand{\hs}[1]{\texttt{#1}}
65: \newcommand*\vect[1]{\mathbf{#1}}
66: \newcommand*\mean[1]{\overline{#1}}
67: \newcommand{\argmin}{\operatornamewithlimits{argmin}}
68: \newcommand{\feature}[1]{\phi(#1)}
69: \newcommand{\id}[1]{\texttt{"#1"}}
70: \newcommand{\vlocal}[1]{\CVar\ (\CLocal\ \id{#1})}
71: \newcommand{\vglobal}[1]{\CVar\ (\CGlobal\ \id{#1})}
72: \newcommand{\cat}{\mbox{\ensuremath{+\!\!+\,}}}
73:
74: % Shorthand for our diagrams
75: \newcommand{\CVar}{\texttt{Var}}
76: \newcommand{\CLit}{\texttt{Lit}}
77: \newcommand{\CApp}{\texttt{App}}
78: \newcommand{\CLam}{\texttt{Lam}}
79: \newcommand{\CLet}{\texttt{Let}}
80: \newcommand{\CCase}{\texttt{Case}}
81: \newcommand{\CType}{\texttt{Type}}
82: \newcommand{\CLocal}{\texttt{Local}}
83: \newcommand{\CGlobal}{\texttt{Global}}
84: \newcommand{\CConstructor}{\texttt{Constructor}}
85: \newcommand{\CLitNum}{\texttt{LitNum}}
86: \newcommand{\CLitStr}{\texttt{LitStr}}
87: \newcommand{\CAlt}{\texttt{Alt}}
88: \newcommand{\CDataAlt}{\texttt{DataAlt}}
89: \newcommand{\CLitAlt}{\texttt{LitAlt}}
90: \newcommand{\CDefault}{\texttt{Default}}
91: \newcommand{\CNonRec}{\texttt{NonRec}}
92: \newcommand{\CRec}{\texttt{Rec}}
93: \newcommand{\CBind}{\texttt{Bind}}
94:
95: \begin{document}
96:
97: \mainmatter % start of an individual contribution
98:
99: % first the title is needed
100: \title{Scaling Theory Exploration Through Bucketing}
101:
102: % a short form should be given in case it is too long for the running head
103: \titlerunning{Improving Haskell Theory Exploration}
104:
105: % the name(s) of the author(s) follow(s) next
106: %
107: % NB: Chinese authors should write their first names(s) in front of
108: % their surnames. This ensures that the names appear correctly in
109: % the running heads and the author index.
110: %
111: \author{Chris Warburton%
112: \and Ekaterina Komendantskaya}
113: %
114: \authorrunning{Improving Haskell Theory Exploration}
115: % (feature abused for this document to repeat the title also on left hand pages)
116:
117: % the affiliations are given next; don't give your e-mail address
118: % unless you accept that it will be published
119: \institute{University of Dundee,\\
120: \mailsa\\
121: \url{http://tocai.computing.dundee.ac.uk}}
122:
123: %
124: % NB: a more complex sample for affiliations and the mapping to the
125: % corresponding authors can be found in the file "llncs.dem"
126: % (search for the string "\mainmatter" where a contribution starts).
127: % "llncs.dem" accompanies the document class "llncs.cls".
128: %
129:
130: %\toctitle{Lecture Notes in Computer Science}
131: \tocauthor{Scaling Theory Exploration Through Bucketing}
132: \maketitle
133:
134: \begin{abstract}
135: Mathematical Theory Exploration can discover novel, interesting properties of
136: formal definitions (such as a mathematical theory, scientific model or
137: computer program). In principle this is a fully automated process, but in
138: practice requires careful selection of definitions to avoid infeasible running
139: times when more than a few dozen definitions are provided.
140:
141: We call this cherry-picking the \emph{bucketing problem}, and demonstrate its
142: necessity empirically by exploring definitions sampled from a theorem-proving
143: corpus; finding that problematic definitions severely increase the variance in
144: running time with size, despite the median remaining low. We measure the
145: effect of bucketing on the number of desirable theorems that remain possible
146: to discover, finding a large gap between best- and worst-case selections,
147: indicating the potential for smart bucketing strategies to avoid impacting
148: exploration potential too severely. We compare bucketing to \emph{clustering}
149: (grouping based on similarity), and find solutions to the latter perform no
150: better than random; indicating the difficulty of this open problem.
151: \end{abstract}
152:
153: \input{intro.tex}
154: \input{background.tex}
155: \input{contributions.tex}
156: \input{sizes.tex}
157: \input{implementation.tex}
158: \input{evaluation.tex}
159: \input{related.tex}
160: \input{conclusion.tex}
161:
162: \bibliographystyle{plain}
163: \bibliography{Bibtex}
164:
165: \input{appendices.tex}
166:
167: \end{document}
Generated by git2html.