bartefil.tex

\documentclass[twoside]{ctuthesis}

% Instructions:
% [Disertační práce - formální náležitosti](https://intranet.fel.cvut.cz/cz/vv/doktorandi/dis.html)
% [Směrnice děkana pro obhajoby disertačních prací](https://intranet.fel.cvut.cz/cz/vv/doktorandi/predpisy/SmobhDIS.pdf)
% [Řád doktorského studia](https://intranet.fel.cvut.cz/cz/rozvoj/rad-doktorskeho-studia.pdf)
% [Studijní řád ČVUT](https://intranet.fel.cvut.cz/cz/rozvoj/studijni-rad.pdf)
% [Žádost o obhajobu](https://intranet.fel.cvut.cz/cz/vv/doktorandi/formulare/Zadostoobhajobu.pdf)
% [Dean's Directive](https://intranet.fel.cvut.cz/en/education/rules/SD_defence.pdf)

\input{preamble}

% ctuthesis does not set the PDF metadata correctly.
\hypersetup{
    pdftitle={Machine Learning for Saturation-Based Theorem Proving},
    pdfauthor={Mgr. Filip Bártek},
    pdfsubject={Dissertation Thesis},
    pdfkeywords={automatic theorem proving, machine learning}
}

\glsdisablehyper
\presetkeys{todonotes}{disable}{}

% LNCS: Words in a heading that are joined by a hyphen are subject to a special rule. If the first word can stand alone, the second word should be capitalized.

\begin{document}

% Ensure that my publications are referenced with the lowest reference numbers.
\input{nocites}

%a) On the title page or the first page
%i) the identification of the university, faculty and supervising department.
%ii) the title of the dissertation,
%iii) the “Dissertation thesis” indication,
%iv) the name of the candidate,
%v) the year of the dissertation submission,
%vi) the name of the supervisor,
%vii) the study program,
%viii) the study branch,
%b) a one-page summary in the language of the dissertation as well as in the Czech and English languages,

%a) na titulní nebo prvé straně
%i) označení vysoké školy, fakulty a školícího pracoviště,
%ii) název práce,
%iii) označení „Disertační práce“,
%iv) jméno disertanta,
%v) rok podání práce,
%vi) jméno školitele
%vii) studijní program,
%viii) obor studia,
%b) jednostránkovou anotaci v jazyce práce a současně jazyce českém a anglickém,

\maketitle

\todo[inline]{Resolve warnings: \enquote{name\{glo:*\} has been referenced but does not exist, replaced by a fixed one}}

\todo[inline]{Clarify terms: TPTP, Vampire, search space, superposition-based ATP, parameterized problem solving (?), proof search (as training data point, as process), problem (input problem), \gls{sot}, superposition inference, literal selection, inference, KBO, combinatorial explosion of proof search, heuristics, strategy scheduling, strategy optimization, complementary strategies}

\todo[inline]{Ideas: "ATP is important" - provers, ... MLTP is quite established (?) - AITP conference ...}
\todo[inline]{Discuss prominent successes of machine-assisted proving. Bill McCune w/ Otter - Robbins algebra problem. Sledgehammer. Software verification. Draw inspiration from Urban, Jasmin.}
\todo[inline]{Ensure the introduction reads like a story.}

\todo[inline]{
ATPing has solved many useful problems. It's a cool technology.

Since ATPing is hard, it uses heuristics.

The heuristics are traditionally tuned by humans. ML has been used increasingly to improve ATP performance.

How to do ML for ATP? - Proof search guidance, HPO.
}

\todo[inline]{Justify: \enquote{Vampire represents the state of the art of \gls{atping}.} Justify by CASC report etc.}

\glsresetall
\input{chapters/introduction}

\todo[inline]{Describe related work.}

\input{chapters/results}
\input{chapters/conclusion}
\input{chapters/genai}

\bibliography{bartefil}

\appendix

\input{chapters/publications}

%\printglossaries
\todo[inline]{Clean up and include the glossary.}

\ctutemplate{specification.as.chapter}

\end{document}