cite zip

Author: hargoniX

presentation/literature.bib

@@ -90,3 +90,17 @@ @inbook{subsume
   year = {1998},
   pages = {427–441}
 }
+
+@phdthesis{zipperposition,
+  author       = {Simon Cruanes},
+  title        = {Extending Superposition with Integer Arithmetic, Structural Induction,
+                  and Beyond. (Extensions de la Superposition pour l'Arithm{'{e}}tique
+                  Lin{'{e}}aire Enti{`{e}}re, l'Induction Structurelle, et bien
+                  plus encore)},
+  school       = {{'{E}}cole Polytechnique, Palaiseau, France},
+  year         = {2015},
+  url          = {https://tel.archives-ouvertes.fr/tel-01223502%7D,
+  timestamp    = {Tue, 21 Jul 2020 00:40:37 +0200},
+  biburl       = {https://dblp.org/rec/phd/hal/Cruanes15.bib%7D,
+  bibsource    = {dblp computer science bibliography, https://dblp.org}/
+}

presentation/presentation.typ

@@ -213,7 +213,7 @@ Uses the rules and side conditions from @braniac:
 - configurable literal selection:
   - none
   - first negative literal
-  - all positive literals and first negative maximal literal (zipperposition default)
+  - all positive literals and first negative maximal literal (@zipperposition default)
 
 == Simplifications and Tautology Check
 For simplification rules:
@@ -232,7 +232,7 @@ For tautology checking:
 Heuristic based on @subsume:
 - order literals to work likely harder ones earlier
 - afterwards bruteforce using an efficient backtracking
-  scheme like in zipperposition
+  scheme like in @zipperposition
 - uses a feature vector index for forward/backward substitution
 
 = Performance