%PDF-1.7
%
1 0 obj
<<
/Metadata 2 0 R
/Type /Catalog
/Outlines 3 0 R
/Pages 4 0 R
>>
endobj
5 0 obj
<<
/Keywords (proof search; tactic; Lean; interactive theorem proving; deductive verification; type theory)
/Creator (LaTeX with acmart 2022/04/09 v1.84 Typesetting articles for the Association for Computing Machinery and hyperref 2021-02-27 v7.00k Hypertext links for LaTeX; Conference Publishing Consulting)
/ModDate (D:20230118032728-08'00')
/CreationDate (D:20221231133354+01'00')
/Producer (pdfTeX, Version 3.141592653-2.6-1.40.22 \(TeX Live 2021 Gentoo Linux\) kpathsea version 6.3.3; ConfPub - poplws23cppmain-p18-p rev-2b5efd80dd-62534:62535 p253; modified using iText 4.2.0 by 1T3XT)
/Subject (- Mathematics of computing -> Mathematical software; - Theory of computation -> Type theory; Logic and verification; Automated reasoning;; CPP 2023)
/PTEX.Fullbanner (This is pdfTeX, Version 3.141592653-2.6-1.40.22 \(TeX Live 2021 Gentoo Linux\) kpathsea version 6.3.3)
/Author <4A616E6E6973204C696D7065726720616E6420417374612048616C6B6AE6722046726F6D>
/Title (Aesop: White-Box Best-First Proof Search for Lean)
>>
endobj
2 0 obj
<<
/Length 3677
/Subtype /XML
/Type /Metadata
>>
stream
pdfTeX, Version 3.141592653-2.6-1.40.22 (TeX Live 2021 Gentoo Linux) kpathsea version 6.3.3; ConfPub - poplws23cppmain-p18-p rev-2b5efd80dd-62534:62535 p253; modified using iText 4.2.0 by 1T3XT
2023-01-18T03:27:28-08:00
2023-01-11T18:10:33+01:00
LaTeX with acmart 2022/04/09 v1.84 Typesetting articles for the Association for Computing Machinery and hyperref 2021-02-27 v7.00k Hypertext links for LaTeX
Aesop: White-Box Best-First Proof Search for Lean- Mathematics of computing -> Mathematical software; - Theory of computation -> Type theory; Logic and verification; Automated reasoning;
endstream
endobj
3 0 obj
<<
/Type /Outlines
/Count 30
/First 6 0 R
/Last 7 0 R
>>
endobj
4 0 obj
<<
/Kids [8 0 R 9 0 R 10 0 R 11 0 R 12 0 R 13 0 R 14 0 R 15 0 R 16 0 R 17 0 R
18 0 R 19 0 R 20 0 R 21 0 R 22 0 R]
/Type /Pages
/Count 15
/ITXT (4.2.0)
>>
endobj
6 0 obj
<<
/Dest [9 0 R /Fit]
/Next 23 0 R
/Parent 3 0 R
/Title (Abstract)
>>
endobj
7 0 obj
<<
/Dest [22 0 R /Fit]
/Parent 3 0 R
/Title (References)
/Prev 24 0 R
>>
endobj
8 0 obj
<<
/Contents 25 0 R
/Type /Page
/Resources <<
/Font <<
/F1 26 0 R
/F2 27 0 R
/F3 28 0 R
>>
/XObject <<
/Xf1 29 0 R
>>
>>
/Annots [30 0 R 31 0 R 32 0 R]
/Parent 4 0 R
/MediaBox [0 0 595 842]
>>
endobj
9 0 obj
<<
/Contents 33 0 R
/Type /Page
/Resources <<
/ExtGState 34 0 R
/ProcSet [/PDF /ImageC /Text]
/Font 35 0 R
/XObject 36 0 R
>>
/Annots [37 0 R 38 0 R 39 0 R 40 0 R 41 0 R 42 0 R 43 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
10 0 obj
<<
/Contents 44 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 45 0 R
>>
/Annots [46 0 R 47 0 R 48 0 R 49 0 R 50 0 R 51 0 R 52 0 R 53 0 R 54 0 R 55 0 R
56 0 R 57 0 R 58 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
11 0 obj
<<
/Contents 59 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 60 0 R
>>
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
12 0 obj
<<
/Contents 61 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 62 0 R
>>
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
13 0 obj
<<
/Contents 63 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 64 0 R
>>
/Annots [65 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
14 0 obj
<<
/Contents 66 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 67 0 R
>>
/Annots [68 0 R 69 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
15 0 obj
<<
/Contents 70 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 71 0 R
>>
/Annots [72 0 R 73 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
16 0 obj
<<
/Contents 74 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 75 0 R
>>
/Annots [76 0 R 77 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
17 0 obj
<<
/Contents 78 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 79 0 R
>>
/Annots [80 0 R 81 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
18 0 obj
<<
/Contents 82 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 83 0 R
>>
/Annots [84 0 R 85 0 R 86 0 R 87 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
19 0 obj
<<
/Contents 88 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 89 0 R
>>
/Annots [90 0 R 91 0 R 92 0 R 93 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
20 0 obj
<<
/Contents 94 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 95 0 R
>>
/Annots [96 0 R 97 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
21 0 obj
<<
/Contents 98 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 99 0 R
>>
/Annots [100 0 R 101 0 R 102 0 R 103 0 R 104 0 R 105 0 R 106 0 R 107 0 R 108 0 R 109 0 R
110 0 R 111 0 R 112 0 R 113 0 R 114 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
22 0 obj
<<
/Contents 115 0 R
/Type /Page
/Resources <<
/ProcSet [/PDF /Text]
/Font 116 0 R
>>
/Annots [117 0 R 118 0 R 119 0 R 120 0 R 121 0 R 122 0 R 123 0 R 124 0 R 125 0 R 126 0 R
127 0 R 128 0 R 129 0 R 130 0 R 131 0 R 132 0 R 133 0 R 134 0 R 135 0 R 136 0 R
137 0 R 138 0 R 139 0 R 140 0 R 141 0 R 142 0 R 143 0 R 144 0 R 145 0 R 146 0 R
147 0 R 148 0 R 149 0 R 150 0 R 151 0 R 152 0 R]
/Parent 4 0 R
/Rotate 0
/MediaBox [0 0 612 792]
>>
endobj
23 0 obj
<<
/Dest [9 0 R /Fit]
/Next 153 0 R
/Parent 3 0 R
/Title (1 Introduction)
/Prev 6 0 R
>>
endobj
24 0 obj
<<
/Dest [22 0 R /Fit]
/Next 7 0 R
/Parent 3 0 R
/Title (Acknowledgments)
/Prev 154 0 R
>>
endobj
25 0 obj
<<
/Length 628
/Filter /FlateDecode
>>
stream
xUr0+Ϊ%3`ҕ%!
ŖA$"iPt<;s=WG~r3Ovd+>wΝ䜧 ME*Y\ąMi
rG>bU)9sC/iB|`"M^9KY!ABXe4m8JFL*=%2cJ$ƿI$cZS9kp{L/M$J\z;vyX2570tŵG RdLzN>54Hm벗H7JN4,1a@f3$Y)oWVIƌ/͖+D'+ s}è^Pc*M_ُo9ߡu][ɇ"۬(L2;cdw[pY*7Q5ry$̈́HVMo~mt+R`xVi#$3܁cz>ě..Or^3q1>=q䎌]W~աÿ1>oz"V"'JmnT;kׁX7d ٜq*\۹`_ə
endstream
endobj
26 0 obj
<<
/Subtype /Type1
/Type /Font
/BaseFont /Helvetica
/Encoding /WinAnsiEncoding
>>
endobj
27 0 obj
<<
/Subtype /Type1
/Type /Font
/BaseFont /Helvetica-Bold
/Encoding /WinAnsiEncoding
>>
endobj
28 0 obj
<<
/Subtype /Type1
/Type /Font
/BaseFont /Helvetica-Oblique
/Encoding /WinAnsiEncoding
>>
endobj
29 0 obj
<<
/Length 1707
/Subtype /Form
/Filter /FlateDecode
/Type /XObject
/Matrix [1 0 0 1 0 0]
/FormType 1
/Resources <<
/ExtGState <<
/GS7 155 0 R
/GS10 156 0 R
>>
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Meta18 157 0 R
/Image5 158 0 R
>>
/Font <<
/F1 159 0 R
/F2 160 0 R
/F3 161 0 R
>>
>>
/BBox [0 0 595.32 841.92]
>>
stream
xZ[o6~7GXhQD(eV]=CŖ&r^EYt 2lh*ټB/_N_UU6t6_O٪(ؖ/Jg~s~G!猠%"q8%XD&zx4}xEBD8bS
VylG0Zv(nn+llz CfhFIvC&6!P9z?}6)+~ VkyXU'yN&up j H:)Uuآ66B>p@4bN-֒IiR굄g
dVIjuKkKaz
rP
s)Yœ'9+ZAD#* X
zO)]kGX1tPz*ћ̰cQх%4>̀pVqLkFs55SY'}R5HB1;^;#f]Y;-7(7PQ:J گ2%ZU9!=Q(6;ʃͳ(GK^9
+&^Xk#&Ol2s"wfPǵ:R
:_^*a̧ՈN0jK'CݷD!;W(HG0e7bK.v&O]9标S!|xq!^RHg2?gM{)OA>]tpmSRf~qkì(lN薁hr0o`BLgyYpH^m!<4??ct'd~Z
fιmc@ENL}(L;#)Q'ǥiC57ڮ)Lѷݣ:reumEaZEFm۵Ss].[-
[Oh. SlxGwmow sg0]zǁX'{-TyͩL~N38s|,锑ER{#ˈD,w#[6F
J𗒫auꅡcT($*@.^5tDv9`S>`a ~p ^{ma]w#]q>S!):t)`dOԙ]r[έ]WkYty\$KbQȵ+Wo/
^7ڶXKk^7wޓ{). m͎nm2G}f'ݩVij3| UV2z ݖrL_ʸYbٟmiB묐fSmh<槸*is-լ+NCBs5O.%8:(azS>$>
/Subtype /Link
/C [0 0 1]
/Border [0 0 0]
/Rect [57 458 176.54 468]
>>
endobj
31 0 obj
<<
/A <<
/S /URI
/URI (https://orbit.dtu.dk/en/publications/96c36815-efd7-4746-b6b7-f1ddf324e5cf)
>>
/Subtype /Link
/C [0 0 1]
/Border [0 0 0]
/Rect [57 348 158.14 358]
>>
endobj
32 0 obj
<<
/A <<
/S /URI
/URI (https://doi.org/10.1145/3573105.3575671)
>>
/Subtype /Link
/C [0 0 1]
/Border [0 0 0]
/Rect [159.81 258 342.72 268]
>>
endobj
33 0 obj
<<
/Length 6937
/Filter /FlateDecode
>>
stream
x<˒uzUQR,RSM\hl)cdE3%9UhÆ$(Ԩ:|D!|G>Hr, 뼟YZO_oqq|s/>|uR-tW.^<.f2ץ^|=]*EYe8?Xm1ԭ>>̾oeUa7N8weiYG]gr_f/6~]I.{=(~sW7@